Trying to use an anonymous type function (higher order functions are not supported yet)
module Test with letrec id [a : Data] (x : a) : a = x foo (_ : Unit) : Unit = do id (/\a. \(x : a). x) () Fragment violation when converting Tetra module to Salt module. Cannot convert expression. Cannot convert type abstraction in this context. The program must be lambda-lifted before conversion. with: /\(a : Data). \(x : a). x
Trying to use higher kinded type arguments (which need an 'Any' region to implement safely, in general)
module Test data List (a : Data) where Nil : a -> List a Cons : a -> List a -> List a with letrec foo [a : Data ~> Data] [b : Data] (x : b) : b = x bar (_ : Unit) : Nat# = foo [List] [Nat#] 5# Cannot convert expression. Unsupported type argument to function or constructor. In particular, we don't yet handle higher kinded type arguments. See [Note: Salt conversion for higher kinded type arguments] in the implementation of the Tetra to Salt conversion. with: [List]
Trying to partially apply a primitive operator:
module Test with letrec thing (_ : Unit) : Nat# -> Nat# = add# [Nat#] 5# Fragment violation when converting Tetra module to Salt module. Cannot convert expression. Partial application of primitive operators is not supported. with: add# [Nat#] 5#
In contrast, the old ddc-alpha compiler (which I wrote for my PhD work), would signal its displeasure with partially applied primops by producing a program that segfaulted at runtime. We turn our backs on the bad old days.
Nested Data TypesPleasingly, the new type inferencer does seem to work with some non-standard programs -- even though these don't compile all the way to object code yet. Here is a Core Tetra program using nested data types:
module Test data Tuple2 (a b : Data) where T2 : a -> b -> Tuple2 a b data Nest (a : Data) where NilN : Nest a ConsN : a -> Nest (Tuple2 a a) -> Nest a with letrec thing (_ : Unit) = ConsN 7# (ConsN (T2 1# 2#) (ConsN (T2 (T2 6# 7#) (T2 7# 4#)) NilN))This example is based on one from the Bird and Meertens 1998 paper. Note that the second argument of the ConsN constructor takes a Nest where the element type is more complex than the original parameter. The type inference algorithm in the alpha compiler would have diverged on this program.
Higher Rank TypesI've also tried out some simple examples with higher ranked types, here is one:
module Test with letrec thing1 (blerk : ([a : Data]. a -> a) -> Nat#) : Nat# = blerk (/\a. \(x : a). x) thing2 (u : Unit) = thing1 (\(f : [a : Data]. a -> a). f 5#)thing1 has a rank-3 type because it is a function, that takes a function, that takes a function which is polymorphic. There is a quantifier that appears at depth 3 contravariantly. Writing the type of thing1 in full makes this easier to see:
thing1 :: ((([a : Data]. a -> a) -> Nat#) -> Nat#Again, I can't compile this example to object code yet because code generation for higher order functions isn't finished. However, type inference is a separate concern, and I don't know of any remaining problems in this part.