[mercury-users] I can't see what this error message is trying to tell me.

[Mark Brown]

Hi Michael,

On 23-Apr-2012, Michael Richter <ttmrichter at gmail.com> wrote:
> ../src/decimal.m:279: In clause for function `radix'/0:
> ../src/decimal.m:279:   in function result term of clause head:
> ../src/decimal.m:279:   in argument 4 of functor `number/4':
> ../src/decimal.m:279:   type error in unification of argument
> ../src/decimal.m:279:   and constant `basic_default_context'.
> ../src/decimal.m:279:   argument has type `(some [C] C)',
> ../src/decimal.m:279:   constant `basic_default_context' has type `(some [C]
> ../src/decimal.m:279:   C)'.
> ../src/decimal.m:279:   The partial type assignment was:
> ../src/decimal.m:279:     some [C_1]
> ../src/decimal.m:279:     HeadVar__1_1: decimal.decimal(C)
> ../src/decimal.m:279:     V_2: decimal.sign
> ../src/decimal.m:279:     V_3: integer.integer
> ../src/decimal.m:279:     V_4: integer.integer
> ../src/decimal.m:279:     V_5: C
> ... error log truncated, see `decimal.err' for the complete log.
> 
> So, the argument is type (some [C] C) and the constant being passed in is
> type (some [C] C) and this is somehow a problem.  I don't get it.

In my left hand I have some type of fruit.  In my right hand I have some type
of fruit.  Can you conclude from that that the pieces of fruit I am holding
are the same type?  No, because there's two occurrences of the "some"
quantifier and they bind the actual types independently.  One could be a
papaya and the other a pomegranate.

The compiler is trying to tell you something along those lines, only it's
a bit hard to say because both types are called C.  You need to keep in
mind that each quantifier introduces a new type variable, so those Cs
are actually two separate variables that happen to have the same name.

This error most commonly arises when field syntax is used with an
existentially typed data constructor.  For example, if you write

    F1 = X ^ field1,
    F2 = X ^ field2

where X is of type x:

    :- type x ---> some [T] f(field1::T, field2::T).

then this counts as two separate deconstructions, hence there are two
quantifiers around the types of F1 and F2, and the compiler will not
treat them as having the same type.  To prove to the compiler that the
types are the same, you need to write

    X = f(F1, F2)

Hope this helps.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------