Opened 3 years ago

Closed 3 years ago

#375 closed defect (fixed)

Better inference with higher kinded type constructors.

Reported by: benl Owned by:
Priority: normal Milestone: 0.4.3
Component: Source Type Inferencer Version: 0.4.2
Keywords: Cc:

Description

In Data.Functor this works

data Functor (f: Data -> Data) where
        Functor: ([a b: Data]. (a -> b) -> f a -> f b) -> Functor f

fmap ((Functor fmap'): Functor f): (a -> b) -> f a -> f b
 = fmap'

But with a separate signature it does not.

fmap    : [a b: Data]. [f: Data ~> Data]
        . Functor f -> (a -> b) -> f a -> f b
fmap (Functor fmap') = fmap'

* Compiling packages/ddc-code/tetra/base/Class/Functor.ds
Error in transformed module.
  Type function used in application has invalid kind.
      In application: ?2 ?5
   cannot apply type: ?2
             of kind: Data
             to type: ?5

The kind of the existential isn't being set right.

Change History (1)

comment:1 Changed 3 years ago by benl

  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.