Quantcast

Data Kinds and superfluous (in my opinion) constraints contexts

classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Data Kinds and superfluous (in my opinion) constraints contexts

Serguey Zefirov
I decided to take a look at DataKinds extension, which became
available in GHC 7.4.

My main concerns is that I cannot close type classes for promoted data
types. Even if I fix type class argument to a promoted type, the use
of encoding function still requires specification of context. I
consider this an omission of potentially very useful feature.

Example is below.
-----------------------------------------------------------------------------------------
{-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
UndecidableInstances #-}
{-# LANGUAGE GADTs #-}

-- a binary numbers.
infixl 5 :*
data D =
                D0
        | D1
        | D :* D
        deriving Show

-- encoding for them.
data EncD :: D -> * where
        EncD0 :: EncD D0
        EncD1 :: EncD D1
        EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)

-- decode of values.
fromD :: D -> Int
fromD D0 = 0
fromD D1 = 1
fromD (d :* d0) = fromD d * 2 + fromD d0

-- decode of encoded values.
fromEncD :: EncD d -> Int
fromEncD EncD0 = 0
fromEncD EncD1 = 1
fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b

-- constructing encoded values from type.
-- I've closed possible kinds for class parameter (and GHC
successfully compiles it).
-- I fully expect an error if I will try to apply mkD to some type
that is not D.
-- (and, actually, GHC goes great lengths to prevent me from doing that)
-- By extension of argument I expect GHC to stop requiring context
with MkD a where
-- I use mkD "constant function" and it is proven that a :: D.
class MkD (a :: D) where
        mkD :: EncD a
instance MkD D0 where
        mkD = EncD0
instance MkD D1 where
        mkD = EncD1
-- But I cannot omit context here...
instance (MkD a, MkD b) => MkD (a :* b) where
        mkD = EncDStar mkD mkD

data BV (size :: D) where
        BV :: EncD size -> Integer -> BV size

bvSize :: BV (size :: D) -> Int
bvSize (BV size _) = fromEncD size

-- ...and here.
-- This is bad, because this context will arise in other places, some of which
-- are autogenerated and context for them is incomprehensible to human
-- reader.
-- (they are autogenerated precisely because of that - it is tedious
and error prone
-- to satisfy type checker.)
fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
-- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work,
but is not that useful.
fromIntgr int = BV mkD int
-----------------------------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Data Kinds and superfluous (in my opinion) constraints contexts

Simon Peyton Jones
I'm glad you've been trying out kinds.  However, I don't understand the feature you want here.

You say:

fromIntgr :: Integer -> BV (size :: D)
fromIntgr int = BV mkD int   -- doesn't work, but desired.

fromIntgr :: MkD size => Integer -> BV (size :: D)
fromIntgr int = BV mkD int   -- does work, but is not that useful.

The implementation MUST pass a value parameter for (MkD size =>) to fromIntgr. Your point is presumably that since every inhabitant of kind D is an instance of MkD, the (MkD size =>) doesn't actually constrain the type at all. It really works for every instantiation of 'size'.

So maybe your feature is

  Please omit class constraints where I can see that
  every suitably-kinded argument is an instance of the
  class.

I suppose that might be conceivable, but it'd make the language more complicated, and the implementation, and I don't see why the second version is "not that useful".

Start a feature-request ticket if you like, though.

Simon

| -----Original Message-----
| From: [hidden email] [mailto:haskell-cafe-
| [hidden email]] On Behalf Of Serguey Zefirov
| Sent: 06 May 2012 17:49
| To: haskell
| Subject: [Haskell-cafe] Data Kinds and superfluous (in my opinion)
| constraints contexts
|
| I decided to take a look at DataKinds extension, which became available
| in GHC 7.4.
|
| My main concerns is that I cannot close type classes for promoted data
| types. Even if I fix type class argument to a promoted type, the use of
| encoding function still requires specification of context. I consider
| this an omission of potentially very useful feature.
|
| Example is below.
| ------------------------------------------------------------------------
| -----------------
| {-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
| UndecidableInstances #-} {-# LANGUAGE GADTs #-}
|
| -- a binary numbers.
| infixl 5 :*
| data D =
| D0
| | D1
| | D :* D
| deriving Show
|
| -- encoding for them.
| data EncD :: D -> * where
| EncD0 :: EncD D0
| EncD1 :: EncD D1
| EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)
|
| -- decode of values.
| fromD :: D -> Int
| fromD D0 = 0
| fromD D1 = 1
| fromD (d :* d0) = fromD d * 2 + fromD d0
|
| -- decode of encoded values.
| fromEncD :: EncD d -> Int
| fromEncD EncD0 = 0
| fromEncD EncD1 = 1
| fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b
|
| -- constructing encoded values from type.
| -- I've closed possible kinds for class parameter (and GHC successfully
| compiles it).
| -- I fully expect an error if I will try to apply mkD to some type that
| is not D.
| -- (and, actually, GHC goes great lengths to prevent me from doing that)
| -- By extension of argument I expect GHC to stop requiring context with
| MkD a where
| -- I use mkD "constant function" and it is proven that a :: D.
| class MkD (a :: D) where
| mkD :: EncD a
| instance MkD D0 where
| mkD = EncD0
| instance MkD D1 where
| mkD = EncD1
| -- But I cannot omit context here...
| instance (MkD a, MkD b) => MkD (a :* b) where
| mkD = EncDStar mkD mkD
|
| data BV (size :: D) where
| BV :: EncD size -> Integer -> BV size
|
| bvSize :: BV (size :: D) -> Int
| bvSize (BV size _) = fromEncD size
|
| -- ...and here.
| -- This is bad, because this context will arise in other places, some of
| which
| -- are autogenerated and context for them is incomprehensible to human
| -- reader.
| -- (they are autogenerated precisely because of that - it is tedious and
| error prone
| -- to satisfy type checker.)
| fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
| -- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work, but
| is not that useful.
| fromIntgr int = BV mkD int
| ------------------------------------------------------------------------
| -----------------
|
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe



_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Data Kinds and superfluous (in my opinion) constraints contexts

Conor McBride-2
Hi Simon

On 10 May 2012, at 13:19, Simon Peyton-Jones wrote:

> I'm glad you've been trying out kinds.  However, I don't understand  
> the feature you want here.
>
> You say:
>
> fromIntgr :: Integer -> BV (size :: D)
> fromIntgr int = BV mkD int   -- doesn't work, but desired.
>
> fromIntgr :: MkD size => Integer -> BV (size :: D)
> fromIntgr int = BV mkD int   -- does work, but is not that useful.
>
> The implementation MUST pass a value parameter for (MkD size =>) to  
> fromIntgr. Your point is presumably that since every inhabitant of  
> kind D is an instance of MkD, the (MkD size =>) doesn't actually  
> constrain the type at all. It really works for every instantiation  
> of 'size'.
>
> So maybe your feature is
>
> Please omit class constraints where I can see that
> every suitably-kinded argument is an instance of the
> class.

So we're dealing with the difference between pi and forall. It's
clear that "promotion" alone doesn't really deliver the pi
behaviour. That still currently requires the singleton construction,
which SHE automates, at least in simple cases.

(Shameless plug: see my answer on StackOverflow this morning
http://stackoverflow.com/questions/10529360/recursively-defined-instances-and-constraints)


> I suppose that might be conceivable, but it'd make the language more  
> complicated, and the implementation, and I don't see why the second  
> version is "not that useful".
>
> Start a feature-request ticket if you like, though.

There's a bunch of competing notions to negotiate. Once we have
a promotable type, e.g.,

  data Nat = Zero | Succ Nat

we get a singleton family

  data Natty :: Nat -> * where
    Zeroy :: Natty Zero
    Succy :: Natty n -> Natty (Suc n)

(In fact, SHE has one data family for the singleton construction, and
generates suitable data instance declarations, here mapping Nat to
Natty.)

As Serguey makes clear, we should also get a class like

  class HasNatty :: Nat -> Constraint where
    natty :: Natty n
  instance HasNatty Zero where
    natty = Zeroy
  instance HasNatty n => HasNatty (Succ n) where
    natty = Succy natty

Again, SHE automates this construction. The constraint HasNatty n is
written (with distinctive ugliness) {:n :: Nat:}, as is the witness,
desugaring to the equivalent of (natty :: Natty n).

We can then play spot-the-difference between

(1) forall (n :: Nat).
(2) forall (n :: Nat). Natty n ->
(3) forall (n :: Nat). HasNatty n =>

(1) is genuinely different; (2) and (3) are equivalent but have  
different
pragmatics. (1) does not involve any runtime data, and has stronger
free theorems; (2) involved runtime data passed explicitly and readily
pattern-matched (for which SHE also has a notational convenience); (3)
involves runtime data passed implicitly. (2) is somehow the explicit pi
of dependent type theory (and it's how SHE translates pi); (3) is  
somehow
the "implicit pi"; (1) is somehow the "irrelevant pi" (which is an abuse
of the letter pi, as the notion is an intersection rather than a  
product).

I'd like to be able to (and SHE lets me) write (2) as

pi (n :: Nat).

I'd like to be able to (and SHE doesn't let me) write (3) as

(n :: Nat) =>

I see one main dilemma and then finer variations of style. The dilemma  
is

EITHER  make forall act like pi for promoted datatypes, so that runtime
          witnesses are always present
OR      distinguish pi from forall, and be explicit when runtime  
witnesses
          are present

Traditional type theory does the former but is beginning to flirt with  
the
latter, for reasons (better parametricity, more erasure) that have  
value in
theory and practice. I regard the latter as a better fit with Haskell in
any case.

However, it would be good to automate the singleton construction and
sugar over the problem, and even better to avoid the singleton  
construction
just using Nat data in place of Natty data.

Other dilemmas. If we have have distinct pi and forall, which do we get
when we leave out quantifiers? I'd suggest forall, as somehow the better
fit with silence and the more usual in Haskell, but it's moot. When we  
write

instance Applicative (Vector n)                        -- (X)

we currently mean, morally,

instance forall (n :: Nat). Applicative (Vector n)     -- (X)

which we can't define, because pure needs the length at runtime. But
perhaps we should write

instance pi (n :: Nat). Applicative (Vector n)

or (if this syntax is unambiguous)

instance (n :: Nat) => Applicative (Vector n)

both of which would bring n into scope as a runtime witness susceptible
to case analysis.

There is certainly something to be done (and SHE already does some of  
it,
within the limitations of a preprocessor). I'd be happy to help kick  
ideas
around, if that's useful.

All the best

Conor


>
> Simon
>
> | -----Original Message-----
> | From: [hidden email] [mailto:haskell-cafe-
> | [hidden email]] On Behalf Of Serguey Zefirov
> | Sent: 06 May 2012 17:49
> | To: haskell
> | Subject: [Haskell-cafe] Data Kinds and superfluous (in my opinion)
> | constraints contexts
> |
> | I decided to take a look at DataKinds extension, which became  
> available
> | in GHC 7.4.
> |
> | My main concerns is that I cannot close type classes for promoted  
> data
> | types. Even if I fix type class argument to a promoted type, the  
> use of
> | encoding function still requires specification of context. I  
> consider
> | this an omission of potentially very useful feature.
> |
> | Example is below.
> |  
> ------------------------------------------------------------------------
> | -----------------
> | {-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell,  
> TypeFamilies,
> | UndecidableInstances #-} {-# LANGUAGE GADTs #-}
> |
> | -- a binary numbers.
> | infixl 5 :*
> | data D =
> | D0
> | | D1
> | | D :* D
> | deriving Show
> |
> | -- encoding for them.
> | data EncD :: D -> * where
> | EncD0 :: EncD D0
> | EncD1 :: EncD D1
> | EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)
> |
> | -- decode of values.
> | fromD :: D -> Int
> | fromD D0 = 0
> | fromD D1 = 1
> | fromD (d :* d0) = fromD d * 2 + fromD d0
> |
> | -- decode of encoded values.
> | fromEncD :: EncD d -> Int
> | fromEncD EncD0 = 0
> | fromEncD EncD1 = 1
> | fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b
> |
> | -- constructing encoded values from type.
> | -- I've closed possible kinds for class parameter (and GHC  
> successfully
> | compiles it).
> | -- I fully expect an error if I will try to apply mkD to some type  
> that
> | is not D.
> | -- (and, actually, GHC goes great lengths to prevent me from doing  
> that)
> | -- By extension of argument I expect GHC to stop requiring context  
> with
> | MkD a where
> | -- I use mkD "constant function" and it is proven that a :: D.
> | class MkD (a :: D) where
> | mkD :: EncD a
> | instance MkD D0 where
> | mkD = EncD0
> | instance MkD D1 where
> | mkD = EncD1
> | -- But I cannot omit context here...
> | instance (MkD a, MkD b) => MkD (a :* b) where
> | mkD = EncDStar mkD mkD
> |
> | data BV (size :: D) where
> | BV :: EncD size -> Integer -> BV size
> |
> | bvSize :: BV (size :: D) -> Int
> | bvSize (BV size _) = fromEncD size
> |
> | -- ...and here.
> | -- This is bad, because this context will arise in other places,  
> some of
> | which
> | -- are autogenerated and context for them is incomprehensible to  
> human
> | -- reader.
> | -- (they are autogenerated precisely because of that - it is  
> tedious and
> | error prone
> | -- to satisfy type checker.)
> | fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
> | -- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does  
> work, but
> | is not that useful.
> | fromIntgr int = BV mkD int
> |  
> ------------------------------------------------------------------------
> | -----------------
> |
> | _______________________________________________
> | Haskell-Cafe mailing list
> | [hidden email]
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Data Kinds and superfluous (in my opinion) constraints contexts

Iavor Diatchki
In reply to this post by Serguey Zefirov
Hello,

The context in your example serves an important purpose: it records the fact that the behavior of the function may differ depending on which type it is instantiated with.   This is quite different from ordinary polymorphic functions, such as `const` for example,  which work in exactly the same way, no matter how you instantiate them.   Note that it doesn't matter that we can solve the constraint for all types of kind `D`---the constraint is there because we can't solve it _uniformly_ for all types.

-Iavor
PS: As an aside, these two forms of polymorphism are sometimes called "parametric" (when functions work in the same way for all types), and "ad-hoc" (when the behavior depends on which type is being used).




On Sun, May 6, 2012 at 9:48 AM, Serguey Zefirov <[hidden email]> wrote:
I decided to take a look at DataKinds extension, which became
available in GHC 7.4.

My main concerns is that I cannot close type classes for promoted data
types. Even if I fix type class argument to a promoted type, the use
of encoding function still requires specification of context. I
consider this an omission of potentially very useful feature.

Example is below.
-----------------------------------------------------------------------------------------
{-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
UndecidableInstances #-}
{-# LANGUAGE GADTs #-}

-- a binary numbers.
infixl 5 :*
data D =
               D0
       |       D1
       |       D :* D
       deriving Show

-- encoding for them.
data EncD :: D -> * where
       EncD0 :: EncD D0
       EncD1 :: EncD D1
       EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)

-- decode of values.
fromD :: D -> Int
fromD D0 = 0
fromD D1 = 1
fromD (d :* d0) = fromD d * 2 + fromD d0

-- decode of encoded values.
fromEncD :: EncD d -> Int
fromEncD EncD0 = 0
fromEncD EncD1 = 1
fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b

-- constructing encoded values from type.
-- I've closed possible kinds for class parameter (and GHC
successfully compiles it).
-- I fully expect an error if I will try to apply mkD to some type
that is not D.
-- (and, actually, GHC goes great lengths to prevent me from doing that)
-- By extension of argument I expect GHC to stop requiring context
with MkD a where
-- I use mkD "constant function" and it is proven that a :: D.
class MkD (a :: D) where
       mkD :: EncD a
instance MkD D0 where
       mkD = EncD0
instance MkD D1 where
       mkD = EncD1
-- But I cannot omit context here...
instance (MkD a, MkD b) => MkD (a :* b) where
       mkD = EncDStar mkD mkD

data BV (size :: D) where
       BV :: EncD size -> Integer -> BV size

bvSize :: BV (size :: D) -> Int
bvSize (BV size _) = fromEncD size

-- ...and here.
-- This is bad, because this context will arise in other places, some of which
-- are autogenerated and context for them is incomprehensible to human
-- reader.
-- (they are autogenerated precisely because of that - it is tedious
and error prone
-- to satisfy type checker.)
fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
-- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work,
but is not that useful.
fromIntgr int = BV mkD int
-----------------------------------------------------------------------------------------

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Data Kinds and superfluous (in my opinion) constraints contexts

Serguey Zefirov
2012/5/17 Iavor Diatchki <[hidden email]>:
> Hello,
>
> The context in your example serves an important purpose: it records the fact
> that the behavior of the function may differ depending on which type it is
> instantiated with.   This is quite different from ordinary polymorphic
> functions, such as `const` for example,  which work in exactly the same way,
> no matter how you instantiate them.   Note that it doesn't matter that we
> can solve the constraint for all types of kind `D`---the constraint is there
> because we can't solve it _uniformly_ for all types.

Oh, it was of great matter to me. Because constraints like that get
through type family expressions and make it hard to conceal state that
should satisfy constraints on type family expressions over the type of
the state.

I can write something like that:

data Combinator s a where
    Combinator :: Class (TypeFamExpr s) => ... -> Combinator s a

And I cannot write something like that:
data Combinator a where
    Combinator :: Class (TypeFamExpr s) => .mentions s.. -> Combinator a

If my TypeFamExpr does have type variables, I get a wild type error
messages that mentions partially computed TypeFamExpr as an argument
to constraint.

I can make more detailed example, if you wish.

>
> -Iavor
> PS: As an aside, these two forms of polymorphism are sometimes called
> "parametric" (when functions work in the same way for all types), and
> "ad-hoc" (when the behavior depends on which type is being used).
>
>
>
>
> On Sun, May 6, 2012 at 9:48 AM, Serguey Zefirov <[hidden email]> wrote:
>>
>> I decided to take a look at DataKinds extension, which became
>> available in GHC 7.4.
>>
>> My main concerns is that I cannot close type classes for promoted data
>> types. Even if I fix type class argument to a promoted type, the use
>> of encoding function still requires specification of context. I
>> consider this an omission of potentially very useful feature.
>>
>> Example is below.
>>
>> -----------------------------------------------------------------------------------------
>> {-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, TypeFamilies,
>> UndecidableInstances #-}
>> {-# LANGUAGE GADTs #-}
>>
>> -- a binary numbers.
>> infixl 5 :*
>> data D =
>>                D0
>>        |       D1
>>        |       D :* D
>>        deriving Show
>>
>> -- encoding for them.
>> data EncD :: D -> * where
>>        EncD0 :: EncD D0
>>        EncD1 :: EncD D1
>>        EncDStar :: EncD (a :: D) -> EncD (b :: D) -> EncD (a :* b)
>>
>> -- decode of values.
>> fromD :: D -> Int
>> fromD D0 = 0
>> fromD D1 = 1
>> fromD (d :* d0) = fromD d * 2 + fromD d0
>>
>> -- decode of encoded values.
>> fromEncD :: EncD d -> Int
>> fromEncD EncD0 = 0
>> fromEncD EncD1 = 1
>> fromEncD (EncDStar a b) = fromEncD a * 2 + fromEncD b
>>
>> -- constructing encoded values from type.
>> -- I've closed possible kinds for class parameter (and GHC
>> successfully compiles it).
>> -- I fully expect an error if I will try to apply mkD to some type
>> that is not D.
>> -- (and, actually, GHC goes great lengths to prevent me from doing that)
>> -- By extension of argument I expect GHC to stop requiring context
>> with MkD a where
>> -- I use mkD "constant function" and it is proven that a :: D.
>> class MkD (a :: D) where
>>        mkD :: EncD a
>> instance MkD D0 where
>>        mkD = EncD0
>> instance MkD D1 where
>>        mkD = EncD1
>> -- But I cannot omit context here...
>> instance (MkD a, MkD b) => MkD (a :* b) where
>>        mkD = EncDStar mkD mkD
>>
>> data BV (size :: D) where
>>        BV :: EncD size -> Integer -> BV size
>>
>> bvSize :: BV (size :: D) -> Int
>> bvSize (BV size _) = fromEncD size
>>
>> -- ...and here.
>> -- This is bad, because this context will arise in other places, some of
>> which
>> -- are autogenerated and context for them is incomprehensible to human
>> -- reader.
>> -- (they are autogenerated precisely because of that - it is tedious
>> and error prone
>> -- to satisfy type checker.)
>> fromIntgr :: Integer -> BV (size :: D) -- doesn't work, but desired.
>> -- fromIntgr :: MkD size => Integer -> BV (size :: D) -- does work,
>> but is not that useful.
>> fromIntgr int = BV mkD int
>>
>> -----------------------------------------------------------------------------------------
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Data Kinds and superfluous (in my opinion) constraints contexts

Iavor Diatchki
Hi,

It is quite likely that the error that you are getting with approach 2 is because when you are constructing the `Combinator` value, there is not enough type information to figure out how to solve the constraint (and it sounds like this happens because there is not enough type information to reduce the type function).   The fix depends on the concrete program but it might be something as simple as adding a type signature somewhere.

Note, again, that it is not sufficient to know that the constraint could be solved for any type of the appropriate kind: we need to actually solve the constraint so that we can determine what the program should do.

The difference between the two `data` definitions is that the second one uses a technique called _existential quantification_, which "hides" the type `s`.  If this type appears nowhere else in the surrounding expressions and the constraint could not be solved, then the constraint is ambiguous.   I could explain that in more detail, if it is unclear please ask.

Happy hacking,
-Iavor







On Thu, May 17, 2012 at 4:18 AM, Serguey Zefirov <[hidden email]> wrote:
I can write something like that:

data Combinator s a where
   Combinator :: Class (TypeFamExpr s) => ... -> Combinator s a

And I cannot write something like that:
data Combinator a where
   Combinator :: Class (TypeFamExpr s) => .mentions s.. -> Combinator a

If my TypeFamExpr does have type variables, I get a wild type error
messages that mentions partially computed TypeFamExpr as an argument
to constraint.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Loading...