[GHC] #2855: Surprising type (family) type derived

[GHC]

#2855: Surprising type (family) type derived
---------------------------------+------------------------------------------
    Reporter:  guest             |        Owner:                  
        Type:  feature request   |       Status:  new             
    Priority:  normal            |    Milestone:                  
   Component:  Compiler          |      Version:  6.10.1          
    Severity:  normal            |   Resolution:                  
    Keywords:                    |   Difficulty:  Unknown         
    Testcase:                    |           Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |  
---------------------------------+------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown
  * type:  bug => feature request

Comment:

 I'm afraid these aren't bugs.   They all arise because type synonym
 families (unlike data type families) do not have to be injective.  For
 example you ask re `Bug5` why GHC doesn't get the type
 {{{
 g :: (C a) => D a -> T a
 }}}
 Answer: because that's not the most general type.  The type GHC gives is
 strictly more general.  Suppose
 {{{
 type instance T Int = Char
 type instance T Bool = Char
 }}}
 then `T Int ~ T Bool`, but of course `Int` and `Bool` are different types.

 The other examples you give are more tiresome.  For example:
 {{{
 class C a where
     type T a
     type U a
     x :: U a -> T a

 data D a = D (U a)

 g :: (C a) => D a -> T a
 g (D u) = x u
 }}}
 We know that `(u :: U a)`, but at what type should we call the polymorphic
 function `x`?  Let's say at some type `a1`.  Then since `x` is applied to
 `u` we know that `U a` should be the same type as `U a1`, ''but that does
 not require `a` to be the same type as `a1`'', as we saw above.

 In this case, it's vexing because the only solution to `(U a ~ U a1)`,
 where (i) `a` is a skolem constant, and (ii) no other equality constraints
 are available to solve it, is `a~a1`.  But GHC doesn't do that kind of
 "the only solution" reasoning.  Yet anyway.

 In general, a function with a polymorphic type variable that occurs only
 under a type function is likely to give rise to this kind of trouble.

 We're also thinking about allowing you to declare theat a type function is
 injective, which would solve this problem in a different way.

 I hope that explains it a bit.  I'll leave this open as a feature
 request... perhaps for injective type functions.  (Although I'm not sure
 whether that'd work in your application.)

 Simon

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