[GHC] #2852: Type family checking oddity

[GHC]

#2852: Type family checking oddity
------------------------------+---------------------------------------------
 Reporter:  guest             |          Owner:                  
     Type:  bug               |         Status:  closed          
 Priority:  normal            |      Milestone:                  
Component:  Compiler          |        Version:  6.10.1          
 Severity:  normal            |     Resolution:  worksforme      
 Keywords:                    |       Testcase:                  
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
------------------------------+---------------------------------------------
Changes (by chak):

  * status:  new => closed
  * resolution:  => worksforme

Comment:

 Replying to [ticket:2852 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.

 In the first proposal of associated types, we used to require such a
 context, but subsequently decided that there is really no basis for this
 requirement.  Take this definition:
 {{{
 myid :: T a -> T a
 myid x = x
 }}}
 Why should we require a `C a` context here?  No class methods are used, no
 evidence is needed.

 Also, what if your definition would have been
 {{{
 newtype D a = D (T a)
 }}}
 Then, `D` cannot have a context.

 In the case of associated '''data''' declarations it would actually be
 rather inconvenient to require contexts.  Say, we have
 {{{
 class D a where
   data DT a
 }}}
 We might want to use `DT` partially applied, as in `F D`, where `F :: (*
 -> *) -> *`.  What context should we use here?

 So, the right way to think of an associated type
 {{{
 class C a where
   type T a
 }}}
 is as syntactic sugar for
 {{{
 type family T a
 class C a
 }}}
 It's convenient to bundle families that are defined in lock step with a
 class as an associated types.  You get a warning if you forget to define
 the family instance in a class instance and it highlights the structure of
 your code for a human reader.  (And it allows for associated synonym
 defaults.)  However, there is really nothing semantically deep about
 associating a family with a class.

 > 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.

 You forgot the `:t` in front of the `D True` the first time around.  Works
 fine with me in 6.10.1 and the HEAD:
 {{{
 *Main> :t D True
 D True :: (Bool ~ T a) => D a
 }}}
 So, I think, this was only a typo during the ghci interaction.  Hence,
 closing the ticket.

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