Indexed constraint families

[Simon Peyton-Jones]

I've added some implementation notes to
http://hackage.haskell.org/trac/ghc/wiki/KindFact

They could doubtless do with expansion: please ask away and/or edit.

Simon

| -----Original Message-----
| From: Manuel M T Chakravarty [mailto:mchakravarty at me.com]
| Sent: 10 September 2011 14:16
| To: Simon Peyton-Jones
| Cc: GHC; Dominic Orchard
| Subject: Re: Indexed constraint families
| 
| This is fantastic stuff!! Thanks, Max!
| 
| I wonder about the difference between lifted and unlifted constraints, though.  The
| wiki page doesn't seem to mention it.
| 
| Manuel
| 
| 
| Simon Peyton-Jones:
| 
| > Folks
| >
| > Max has just pushed a patch that adds a major new feature: indexed constraint
| families; see http://hackage.haskell.org/trac/ghc/wiki/KindFact
| >
| > Internally, a big change is that there is no PredTy any more. So TypeRep has gotten
| simpler (hooray).
| >
| > Julien, Dimitrios: this will conflict with your in flight stuff -- but will
| basically make it simpler.
| >
| > Many thanks to Max; and Dominic for expressing the original idea so persuasively.
| >
| > Simon
| >
| >
| > commit 9729fe7c3e54597ccf29c43c8c8ad0eaa2402ced
| > Author: Max Bolingbroke <batterseapower at hotmail.com>
| > Date:   Tue Sep 6 17:22:47 2011 +0100
| >
| >    Implement -XConstraintKind
| >
| >    Basically as documented in http://hackage.haskell.org/trac/ghc/wiki/KindFact,
| >    this patch adds a new kind Constraint such that:
| >
| >      Show :: * -> Constraint
| >      (?x::Int) :: Constraint
| >      (Int ~ a) :: Constraint
| >
| >    And you can write *any* type with kind Constraint to the left of (=>):
| >    even if that type is a type synonym, type variable, indexed type or so on.
| >
| >    The following (somewhat related) changes are also made:
| >     1. We now box equality evidence. This is required because we want
| >        to give (Int ~ a) the *lifted* kind Constraint
| >     2. For similar reasons, implicit parameters can now only be of
| >        a lifted kind. (?x::Int#) => ty is now ruled out
| >     3. Implicit parameter constraints are now allowed in superclasses
| >        and instance contexts (this just falls out as OK with the new
| >        constraint solver)
| >
| >    Internally the following major changes were made:
| >     1. There is now no PredTy in the Type data type. Instead
| >        GHC checks the kind of a type to figure out if it is a predicate
| >     2. There is now no AClass TyThing: we represent classes as TyThings
| >        just as a ATyCon (classes had TyCons anyway)
| >     3. What used to be (~) is now pretty-printed as (~#). The box
| >        constructor EqBox :: (a ~# b) -> (a ~ b)
| >     4. The type LCoercion is used internally in the constraint solver
| >        and type checker to represent coercions with free variables
| >        of type (a ~ b) rather than (a ~# b)
| >
| >
| > _______________________________________________
| > Cvs-ghc mailing list
| > Cvs-ghc at haskell.org
| > http://www.haskell.org/mailman/listinfo/cvs-ghc
|