[GHC] #2852: Type family checking oddity

[GHC]

#2852: Type family checking oddity
-----------------------------+----------------------------------------------
Reporter:  guest             |          Owner:                  
    Type:  bug               |         Status:  new             
Priority:  normal            |      Component:  Compiler        
 Version:  6.10.1            |       Severity:  normal          
Keywords:                    |       Testcase:                  
      Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
-----------------------------+----------------------------------------------
 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2852>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler