[GHC] #3208: Type family panic (taking the IdInfo of a coercion variable)

[GHC]

#3208: Type family panic (taking the IdInfo of a coercion variable)
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:  chak            
        Type:  bug               |       Status:  reopened        
    Priority:  normal            |    Milestone:  6.12 branch     
   Component:  Compiler          |      Version:  6.11            
    Severity:  normal            |   Resolution:                  
    Keywords:                    |   Difficulty:  Unknown         
    Testcase:  T3208a, T3208b    |           Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |  
---------------------------------+------------------------------------------
Changes (by chak):

  * testcase:  T3208 => T3208a, T3208b
  * status:  closed => reopened
  * resolution:  fixed =>

Comment:

 I did fix the original bug, but I noticed another bug in a modified
 version of the program; hence, I'll reopen the ticket.  The problematic
 variant is the same program, but with the inferred types for `fce` and
 `fce'` added as signatures:
 {{{
 {-# LANGUAGE TypeFamilies #-}

 module T3208b where

 class SUBST s where
     type STerm s

 class OBJECT o where
     type OTerm o
     apply :: (SUBST s, OTerm o ~ STerm s) => s -> o

 fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
 fce' f = fce . apply $ f

 fce :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
 fce f = fce' f
 }}}
 In a debugging compiler (compiled with `-DDEBUG`), this violates an
 assertion
 {{{
 ghc-stage1: panic! (the 'impossible' happened)
   (GHC version 6.11.20090807 for i386-apple-darwin):
         ASSERT failed! file compiler/typecheck/TcMType.lhs line 349
 t_afI{tv} [tau]
 }}}
 In a compiler without `-DDEBUG` the program is rejected with the following
 error message:
 {{{
 T3208b.hs:13:0:
     Couldn't match expected type `STerm b'
            against inferred type `OTerm b'
       NB: `OTerm' is a type function, and may not be injective
       NB: `STerm' is a type function, and may not be injective
     When generalising the type(s) for `fce''

 T3208b.hs:13:0:
     Couldn't match expected type `STerm a'
            against inferred type `STerm b'
       NB: `STerm' is a type function, and may not be injective
     When generalising the type(s) for `fce''
 }}}

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