Tricky example: type inferencer is not able to specialise type?

[ilya-klyuchnikov]

An example:

type Boxed a = <Box: a, NoBox: {} >;
type BoxedRecord = {box : Boxed BoxedRecord};

let
  un_box      : forall a. Boxed a -> a -> a
              = x default -> case x of {Box content -> content, NoBox {} -> default};

  un_box_spec : Boxed BoxedRecord -> BoxedRecord -> BoxedRecord
              = un_box;

  un_box_record
              = rec -> un_box rec.box rec

in
  {un_box, un_box_spec, un_box_record}

This is not accepted:

:l "lib/Box2.x"
Occur check fails:
"lib/Box2.x" (line 12, column 24) v695
occurs in
"lib/Box2.x" (line 12, column 31) {box : Boxed v695 | v697}

---

However, just replacing un_box with un_box_spec in the definition of un_box_record is accepted. Note that un_box_spec is the same un_box but with a more special type.

type Boxed a = <Box: a, NoBox: {} >;
type BoxedRecord = {box : Boxed BoxedRecord};

let
  un_box      : forall a. Boxed a -> a -> a
              = x default -> case x of {Box content -> content, NoBox {} -> default};

  un_box_spec : Boxed BoxedRecord -> BoxedRecord -> BoxedRecord
              = un_box;

  un_box_record
              = rec -> un_box_spec rec.box rec

in
  {un_box, un_box_spec, un_box_record}

---

Basically, what I have done manually is just type instantiation.

I understand that this example is a tricky one with "recursive records" and it can be ok to explicitly forbid their usages. But to me it seems that either both variants of this program should be accepted or rejected.

[willtim]

Thanks for the issue report! Type synonyms were added recently and there is indeed a missing cycles check. Synonyms are expanded lazily by the type checker and the occurs check won't see the recursion. Since we don't support recursive types elsewhere, I think the best fix is an upfront check for cycles in the type synonym definitions. I will add this check soon.

[ilya-klyuchnikov]

Thanks for the quick reply and for the great project!

I guess it would be worth to mention more explicitly in the beginning of the README that Expresso doesn't support recursive structural data types.

(There is a note that "Note that records cannot refer to themselves, as Expresso does not support type-level recursion." though - but it is more like a side note).

The thing is that for example Ocaml does support recursive polymorphic variants and the following code is valid for Ocaml compiler:

let un_box box default = match box with
  | `Box content -> content
  | `NoBox -> default

let un_box1 box1 = match box1 with
  | `Box1 content -> content

let un_box2 x = un_box (un_box1 x) x

The types are:

val un_box : [< `Box of 'a | `NoBox ] -> 'a -> 'a = <fun>
val un_box1 : [< `Box1 of 'a ] -> 'a = <fun>
val un_box2 : ([< `Box1 of [< `Box of 'a | `NoBox ] ] as 'a) -> 'a = <fun>

[willtim]

I have added a check to prohibit recursive synonym definitions and updated the README. I'm not sure that recursive records is something I would be keen to try and support, especially given the configuration language use-case that I am exploring. I would rather explore an impredicative type system, which would get us nicer first-class modules and better type singatures for records-as-modules.