[GHC] #12823: Inconsistency in acceptance of equality constraints in different forms

[GHC]

#12823: Inconsistency in acceptance of equality constraints in different forms
-------------------------------------+-------------------------------------
           Reporter:  dfeuer         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  GADTs          |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC accepts
  Unknown/Multiple                   |  invalid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Currently, we (correctly) require a language extension to accept a
 declaration like

     foo :: a ~ b => f a -> f b
     foo x = x

 Suppose I write

 {{{#!hs
 {-# LANGUAGE GADTs, UndecidableInstances, ConstraintKinds #-}
 module A where
 class a ~ b => Equal a b
 instance a ~ b => Equal a b

 type EqualS a b = a ~ b
 }}}

 and then

 {{{#!hs
 -- No extensions
 module B where

 -- This works
 useEqual :: Equal a b => f a -> f b
 useEqual x = x

 -- But this does not
 useEqualF :: EqualF a b => f a -> f b
 useEqualF x = x
 }}}

 It seems that GHC expands type synonyms, but does not reduce constraints,
 before deciding whether enough extensions are in play to allow equality
 constraints. This mismatch feels weird. Is there something about `~`
 proper, and not `Equal`, that triggers the difficulties with let
 generalization? If not, I think they should either both work or both fail
 (probably both fail).

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