Custom Query (358 matches)


Show under each result:

Results (40 - 42 of 358)

Ticket Resolution Summary Owner Reporter
#376 fixed Check variable elaboration in Applicative. benl

When the return type is specified the quantifier is added to the definition:

liftA   (dapp: Applicative f) (f: a -> b) (xa: f a): f b
 = ap dapp (pure dapp f) xa

But removing the return type means the elaborator does not add the quantifier for 'f'

liftA   (dapp: Applicative f) (f: a -> b) (xa: f a)
 = ap dapp (pure dapp f) xa

* Compiling packages/ddc-code/tetra/base/Class/Applicative.ds
Error in transformed module.
  Undefined type variable: f

We also don't get the quantifier if we supply a separate signature for the function.

#375 fixed Better inference with higher kinded type constructors. benl

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.

#371 fixed The status of the last test is not being displayed by the war driver. benl

Current number of tests reported is 226, but we only see the status line for up to 225.

Note: See TracQuery for help on using queries.