Ticket #163 (new defect)

Opened 4 years ago

Elaboration of class constructors isn't respecting their kinds

Reported by: benl Owned by:
Priority: blocker Milestone: 0.1.3
Component: Source Desugarer Version: 0.1.2
Keywords: Cc:

Description

This program should work

class Bag (bag :: % -> * -> *) where
	size 	:: forall a %r1 %r2 
		.  bag %r1 a -(!e1)> Int %r2
		:- !e1 = !Read %r1

instance Bag List where
	size = length

main ()	= println $ show $ size [1, 2, 3];

In the class instance, List has the correct kind, but it's being elaborated to:

instance Bag (List %r1) where
	size = length

which is now an error because (List %r1) has kind * -> * and not % -> * -> *.

The elaborator shouldn't have added the %r1 because that type expression already had the correct kind.

Note: See TracTickets for help on using tickets.