id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
2852,Type family checking oddity,guest,,"Consider the following snipped
{{{
class C a where
    type T a

data D a = D (T a)
}}}
If we now ask for the type of D we get
{{{
> :t D
D :: T a -> D a
}}}
I find this odd.  The type T is in class C, so why is there no context on D saying so?  It would be natural.

Now try some expression
{{{
> D True
<interactive>:1:2:
    Couldn't match expected type `T a' against inferred type `Bool'
    In the first argument of `D', namely `True'
    In the expression: D True
    In the definition of `it': it = D True
}}}
But this isn't really type incorrect, we just don't know yet.  To remedy the problem we can use a context on the data declaration.

{{{
data (C a) => D a = D (T a)
}}}
And we try again
{{{
> :t D True
D True :: (Bool ~ T a, C a) => D a
}}}
This is what I would have expected in the first try as well; a context indicating what must hold for this to be type correct.
",bug,closed,normal,,Compiler,6.10.1,worksforme,,lennart@…,Unknown/Multiple,Unknown/Multiple,,,,,,