[Haskell-cafe] 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 <sergueyz at gmail.com> 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.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120517/c743b5da/attachment.htm>