cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Better translator support for recursion under type constructors

Open IlmariReissumies opened this issue 3 years ago • 0 comments

The translator currently only supports recursion under type constructors for a few hard-coded types pair, option and list.

For a minimal example, consider these types:

Datatype:
  container = Container 'a
End

Datatype:
  thing = NonThing | Thing (thing container)
End

Datatype:
  thing2 = NonThing2 | Thing2 (thing2 option)
End

register_type accepts thing2, but not thing.

The first place where it fails is a tDefine somewhere deep in define_ref_inv, where unless the type constructor is in {pair,option,list}, the recursive invocation of THING_TYPE is not eta-expanded properly before being passed to tDefine.

IlmariReissumies avatar Aug 10 '22 07:08 IlmariReissumies