[m-rev.] for review: Fix abstract equivalence types.

[Peter Wang]

On Wed, 23 Aug 2017 16:59:47 +1000 (AEST), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> The current definition of var is what we call a "notag" type; a type that has
> exactly one function symbol, which has exactly one argument. The type
> checker treats such types differently from the argument's type (in this case,
> it won't allow the unification of a variable with an integer, unless of course
> the integer is wrapped in the var() function symbol), but the code generator
> generates the same code for notag types as for the argument type.
> Therefore the wrapper has no impact whatsoever on either memory
> consumption or execution time.

One advantage of using an abstract equivalence type is that we would not
need to type-specialise predicates and functions for *both* int and var(T).
You'd have to trade that off against the chance of accidental type
mixups in term.m (should be low), and the problem with typeclass
instances.

Another consideration, not yet mentioned, is that the d.u. definition
will cause var terms to be printed differently from int terms, which is
quite helpful in the debugger.

Peter