CODEWITHSUNDEEP
idris
pdxleif
pdxleif

Reputation: 1800

Using heterogenous equality with =

What I have so far is:

module Foo

postulate P : 'P
postulate NP : 'NP

complexityProof : P = NP
complexityProof = ?complexityProof_rhs

But on trying to load the file, I just get:

When elaborating type of Foo.complexityProof:
When elaborating argument y to type constructor =:
    Can't unify
            'NP
    with
            'P

    Specifically:
            Can't unify
                    "NP"
            with
                    "P"

A little suprised at the error, as I thought Idris, having heterogeneous "John Major" equality, was fine with differing types on the left and right-hand side of =. There's a different symbol for that, now?

Upvotes: 5

Views: 393

Answers (1)

Brian McKenna
Brian McKenna

Reputation: 46218

From the documentation:

Note: Idris's equality type is potentially heterogeneous, which means that it is possible to state equalities between values of potentially different types. However, Idris will attempt the homogeneous case unless it fails to typecheck.

You may need to use (~=~) to explicitly request heterogeneous equality.

So I'm not sure why = doesn't work, since I think the docs are trying to say that heterogeneous equality is a fallback, but you can use ~=~ instead:

module Foo

postulate P : 'P
postulate NP : 'NP

complexityProof : P ~=~ NP
complexityProof = ?complexityProof_rhs

Upvotes: 5

Related Questions