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

[Dirk Ziegemeyer]

> Am 23.08.2017 um 10:17 schrieb Peter Wang <novalazy at gmail.com>:
> 
> 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

Thank you for the explanations.

Dirk