cakeml
cakeml copied to clipboard
Better translator support for recursion under type constructors
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.