Opened 5 years ago

Last modified 17 months ago

#323 new feature

Insert type lambdas during inference with higher ranked types.

Reported by: benl Owned by:
Priority: normal Milestone:
Component: Core Type Checker Version: 0.3.2
Keywords: Cc:

Description

From GHC Ticket #1634

t1 :: a -> (forall b. b -> (a,b))
t1 = (,)

With DDC we need to introduce the inner type abstraction explicitly, as inferencer won't do it automatically.

module Test 
data Tuple2 (a : Data) (b : Data) where
 T2 : a -> b -> Tuple2 a b

with letrec
t1 [a : Data] (x : a) : [b : Data]. b -> Tuple2 a b
 = /\(b : Data). T2 [a] [b] x

The core algorithm that DDC's inference is based on can check programs using higher rank types, but we haven't implemented the part that inserts type lambdas into the core program.

Change History (1)

comment:1 Changed 17 months ago by benl

  • Type changed from enhancement to feature
Note: See TracTickets for help on using tickets.