[Hugs-users] explicit kind information; other question

[Ross Paterson]

On Thu, Sep 22, 2005 at 12:02:18PM +0200, luc.duponcheel at accenture.com wrote:
> as an addition to my previous email about dealing with
> 
> > type C ct23 ct12 c1 x y = ct23 (ct12 c1) x y in ...
> 
> > here is what hugs infers
> 
> > :info C
> > -- type constructor with kind (* -> * -> * -> *) -> (* -> *) -> * -> * -> * -> *
> > type C a b c d e = <restricted>
> 
> I see that, from the definition of C only, one cannot really infer a
> more specific kind than the one inferred above.
>
> But, if' C ct23 ct12 c1 x y' (as a synonym for 'ct23 (ct12 c1) x y')
> is used in a context where the expressions 'ct12 c1 x y' and 'c1 x y'
> are used as well, then, the kind inferencer can infer that c1 has kind
> (* -> * -> *), ct12 has kind ((* -> * -> *) -> * -> * -> *), ct12 c1 has
> kind (* -> * -> *), and ct23 has kind ((* -> * -> *) -> * -> * -> *).
>
> So, explicit kind information is not needed if the kind inferencer is
> a bit smarter.

Haskell 98 specifies (Report, 4.6) that kind inference is to be done
on mutually dependent definitions, with polymorphic kinds defaulting
to * (because Haskell lacks kind polymorphism).  As you say, doing kind
inference over the whole module would reduce the need for kind defaulting,
and it seems that GHC 6.4 does this, because it accepts the following
example of an illegal program (from the Report):

	data Tree a  = Leaf | Fork (Tree a) (Tree a)
	type FunnyTree = Tree []     -- invalid

This is rejected by Hugs and older GHC's, as per the Report.

In Haskell 98, one could work around this with tricks like

	type Ignore x y = y
	type ArrowType c t = Ignore [c Int Int] t
	type C ct23 ct12 c1 x y =
		ArrowType c1
		(ArrowType (ct12 c1)
		(ct23 (ct12 c1) x y))

but it seems that Hugs expands type synonyms before doing kind inference,
which is incorrect.