Representing polymorphism with unification-fd

Question

I'd like to use the unification-fd package to implement a simple typechecker for a Hindley-Milner type system. This requires the representation of polymorphic ("forall") types.

What's the best way of representing these types? The variables provided by unification-fd, i.e. the UVar stuff, is for unification (meta)variables, not for variables in the object language. Some possibilities I've pondered:

1. Add a constructor for type variables to my base functor representing types:

   data TyF tcon tv a
       = TCon tcon [a]
       | TVar tv
   

   with zipMatch only unifying equal TVars. Type instantiation consistently replaces every UTerm (TVar a) with a freeVar.

2. (Ab)use UVars for type variables, and replace them with freeVars when instantiating. Requires tracking of universial vs. existential UVars to know which ones to replace.

3. Leave TVar out of TyF, use separate UTerm (TyF tcon) IntVar for monomorpic types during typechecking, UTerm (TyF tcon) tv for polymorphic types visible from the outside, and UTerm (TyF tcon) (Either tv IntVar) during typechecking for intermediate, let-bound variables.

Which would be best? Is there some other way I haven't thought of?

Lochner