Paul Liu | 30 Aug 21:52 2012
Picon

why do I need class context in declaring data constructor?

I had a toy program that encodes simply typed lambda in types. It used
to work fine with GHC prior to 7.2. But now it no longer compiles.
Here is a minimal fragment that demonstrates this problem.

> {-# LANGUAGE GADTs,
>     MultiParamTypeClasses,
>     FlexibleInstances,
>     FlexibleContexts #-}
>
> data Abs env t v where
>   Abs :: g (a, env) h v -> Abs env (g (a, env) h v) (a -> v)
>
> class Eval g env t v where
>   eval :: env -> g env t v -> v
>
> instance Eval g (a, env) h v =>
>          Eval Abs env (g (a, env) h v) (a -> v) where
>   eval env (Abs e) = \x -> eval (x, env) e

The type Abs has 3 parameters: its environment, sub term (encoded in
types), and type. The constructor Abs has 1 parameter: its sub term.
The code loads fine in GHC 7.0.3.

Here is the error reported by GHC 7.2.2 (and later):

test.lhs:14:30:
    Could not deduce (Eval g1 (a1, env) h1 v1)
      arising from a use of `eval'
    from the context (Eval g (a, env) h v)
      bound by the instance declaration at test.lhs:(12,12)-(13,49)
(Continue reading)

Simon Peyton-Jones | 31 Aug 13:37 2012
Picon

Re: why do I need class context in declaring data constructor?

Aha.  See http://hackage.haskell.org/trac/ghc/ticket/7205.

I don't think there's a workaround, I'm afraid

Simon

| -----Original Message-----
| From: haskell-cafe-bounces <at> haskell.org [mailto:haskell-cafe-
| bounces <at> haskell.org] On Behalf Of Paul Liu
| Sent: 30 August 2012 20:52
| To: Haskell Cafe
| Subject: [Haskell-cafe] why do I need class context in declaring data
| constructor?
| 
| I had a toy program that encodes simply typed lambda in types. It used
| to work fine with GHC prior to 7.2. But now it no longer compiles.
| Here is a minimal fragment that demonstrates this problem.
| 
| > {-# LANGUAGE GADTs,
| >     MultiParamTypeClasses,
| >     FlexibleInstances,
| >     FlexibleContexts #-}
| >
| > data Abs env t v where
| >   Abs :: g (a, env) h v -> Abs env (g (a, env) h v) (a -> v)
| >
| > class Eval g env t v where
| >   eval :: env -> g env t v -> v
| >
| > instance Eval g (a, env) h v =>
(Continue reading)

Paul Liu | 31 Aug 20:14 2012
Picon

Re: why do I need class context in declaring data constructor?

Thanks, Simon! I'll be looking forward to its resolution.

On Fri, Aug 31, 2012 at 4:37 AM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> Aha.  See http://hackage.haskell.org/trac/ghc/ticket/7205.
>
> I don't think there's a workaround, I'm afraid
>
> Simon
>
> | -----Original Message-----
> | From: haskell-cafe-bounces <at> haskell.org [mailto:haskell-cafe-
> | bounces <at> haskell.org] On Behalf Of Paul Liu
> | Sent: 30 August 2012 20:52
> | To: Haskell Cafe
> | Subject: [Haskell-cafe] why do I need class context in declaring data
> | constructor?
> |
> | I had a toy program that encodes simply typed lambda in types. It used
> | to work fine with GHC prior to 7.2. But now it no longer compiles.
> | Here is a minimal fragment that demonstrates this problem.
> |
> | > {-# LANGUAGE GADTs,
> | >     MultiParamTypeClasses,
> | >     FlexibleInstances,
> | >     FlexibleContexts #-}
> | >
> | > data Abs env t v where
> | >   Abs :: g (a, env) h v -> Abs env (g (a, env) h v) (a -> v)
> | >
(Continue reading)


Gmane