Typeclass membership doesn't bring coercion superclass requirements into scope

[ryani]

-- This works:
class C1 a where c1 :: a -> Int
class C1 a => C2 a where c2 :: a -> Int
test :: C2 a => a -> Int
test a = c1 a + c2 a

-- This doesn't work:
class (a ~ b) => E a b
cast :: E a b => a -> b
cast a = a

{- error:
tyfam.hs:36:9:
    Couldn't match expected type `b' against inferred type `a'
      `b' is a rigid type variable bound by
          the type signature for `cast' at tyfam.hs:35:14
      `a' is a rigid type variable bound by
          the type signature for `cast' at tyfam.hs:35:12
    In the expression: a
    In the definition of `cast': cast a = a
 -}

I would expect that the requirement of membership in E a b would bring (a ~ b) into scope and allow cast to typecheck.

[ryani]

This is related to a feature request:  http://hackage.haskell.org/trac/ghc/ticket/2101

Here's the motivating example:

type family Cat ts0 ts
type instance Cat ()      ts' = ts'
type instance Cat (s, ts) ts' = (s, Cat ts ts')

class (Cat ts () ~ ts) => Valid ts
instance Valid () -- compiles OK
instance Valid ts => Valid (s, ts) -- fails to compile

-- need to prove Cat (s, ts) () ~ (s, Cat ts ())
-- for the superclass of class Valid.
-- (1) From Valid ts: Cat ts () ~ ts
-- (2) Therefore:     (s, Cat ts ()) ~ (s, ts)

coerce :: forall f ts. Valid ts => f (Cat ts ()) -> f ts
coerce x = x

GHC gives the following two errors:

tyfam.hs:38:0:
    Couldn't match expected type `ts' against inferred type `Cat ts ()'
      `ts' is a rigid type variable bound by
           the instance declaration at tyfam.hs:38:15
    When checking the super-classes of an instance declaration
    In the instance declaration for `Valid (s, ts)'

tyfam.hs:46:11:
    Couldn't match expected type `ts' against inferred type `Cat ts ()'
      `ts' is a rigid type variable bound by
           the type signature for `coerce' at tyfam.hs:45:19
      Expected type: f ts
      Inferred type: f (Cat ts ())
    In the expression: x
    In the definition of `coerce': coerce x = x

[igloo]

Thanks for the report. The example also fails with the HEAD. I don't know what the semantics are meant to be, so I don't know if it's meant to work or not.

[simonpj]

Manuel is working on equality constraints.

[chak]

Sorry, but this one is not going to be fixed for 6.10.1. It requires an extension of the data structure between the type checker and desugarer to get the type-preserving translation right. This is too serious a change to attempt shortly before a release.

[reinerp]

With 7.0.0-rc1 (7.0.0.20100924) and in HEAD, the original testcase reported now compiles successfully (and passes core lint as well).

The motivating example (with coerce) in Ryan's comment also compiles, but fails core lint:

*** Core Lint errors : in result of Desugar ***
<no location info>:
    In the coercion `co_af4'
    co_af4 is out of scope
*** Offending Program ***
T2102.$fValid() [InlPrag=[ALWAYS] CONLIKE] :: T2102.Valid ()
[LclIdX[DFunId], Unf=DFun(arity=0) T2102.D:Valid []]
T2102.$fValid() =
  T2102.D:Valid @ () @ (trans (T2102.TFCo:R:Cat()ts' ()) ())

T2102.$fValid(,) [InlPrag=[ALWAYS] CONLIKE]
  :: forall ts_aaM s_aaN.
     T2102.Valid ts_aaM =>
     T2102.Valid (s_aaN, ts_aaM)
[LclIdX[DFunId], Unf=DFun(arity=3) T2102.D:Valid []]
T2102.$fValid(,) =
  \ (@ ts_aaM) (@ s_aaN) _ ->
    T2102.D:Valid @ (s_aaN, ts_aaM) @ co_af4

T2102.coerce
  :: forall ts_aaJ (f_aaK :: * -> *).
     T2102.Valid ts_aaJ =>
     f_aaK (T2102.Cat ts_aaJ ()) -> f_aaK ts_aaJ
[LclIdX]
T2102.coerce =
  \ (@ ts_aeV)
    (@ f_aeW::* -> *)
    ($dValid_aeX :: T2102.Valid ts_aeV) ->
    case $dValid_aeX of _ { T2102.D:Valid @ co_afa ->
    \ (x_aaL :: f_aeW (T2102.Cat ts_aeV ())) ->
      x_aaL
      `cast` (f_aeW (trans co_afa ts_aeV)
              :: f_aeW (T2102.Cat ts_aeV ()) ~ f_aeW ts_aeV)
    }

*** End of Offense ***

[simonpj]

Sadly, 7.0 does not yet deal with superclass equalities. We are not going to have time to fix this before RC2, but we'll produce a decent error message.

[simonpj]

Hurrah! We now have superclass equalities. I've added this example as a test.

commit 940d1309e58382c889c2665227863fd790bdb21c
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Jun 22 17:37:47 2011 +0100

    Add equality superclasses
    
    Hurrah.  At last we can write
    
       class (F a ~ b) => C a b where { ... }
    
    This fruit of the fact that equalities are now values,
    and all evidence is handled uniformly.
    
    The main tricky point is that when translating to Core
    an evidence variable 'v' is represented either as
      either   Var v
      or       Coercion (CoVar v)
    depending on whether or not v is an equality.  This leads
    to a few annoying calls to 'varToCoreExpr'.

 compiler/basicTypes/MkId.lhs      |    4 +-
 compiler/deSugar/DsExpr.lhs       |   18 +++++++-
 compiler/iface/BuildTyCl.lhs      |   50 ++++++++++------------
 compiler/typecheck/TcInstDcls.lhs |   85 +++++++++++++++++-------------------
 compiler/typecheck/TcMType.lhs    |    9 +----
 compiler/types/Class.lhs          |   21 ++++------
 6 files changed, 92 insertions(+), 95 deletions(-)