Opened 12 years ago

Closed 8 years ago

#2102 closed bug (fixed)

Typeclass membership doesn't bring coercion superclass requirements into scope

Reported by: ryani Owned by: chak
Priority: low Milestone: 7.2.1
Component: Compiler (Type checker) Version: 7.1
Keywords: superclass equalities Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case: indexed_types/should_compile/T2102
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (14)

comment:1 Changed 12 years ago by 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

comment:2 Changed 12 years ago by igloo

Component: CompilerCompiler (Type checker)
difficulty: Unknown
Milestone: 6.10 branch

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.

comment:3 Changed 12 years ago by simonpj

Owner: set to chak

Manuel is working on equality constraints.

comment:4 Changed 11 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:5 Changed 11 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:6 Changed 11 years ago by chak

Keywords: superclass equalities added

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.

comment:7 Changed 10 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:8 Changed 9 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:9 Changed 9 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:10 Changed 9 years ago by reinerp

Type of failure: Compile-time crash
Version: 6.8.27.1

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

comment:11 Changed 9 years ago by 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.

comment:12 Changed 9 years ago by igloo

Milestone: 7.0.17.0.2

comment:13 Changed 9 years ago by igloo

Milestone: 7.0.27.2.1

comment:14 Changed 8 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed_types/should_compile/T2102

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(-)
Note: See TracTickets for help on using tickets.