Using heterogenous equality with =

Question

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?

score 5 · Accepted Answer · answered Jan 04 '15 at 04:41

5

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

answered Jan 04 '15 at 04:41

Brian McKenna

45,528
6
61
60

Thanks for that! It'd be nice to convert that LaTeX doc to an HTML format so Google can index it and we can more easily link to sections of it. – pdxleif Jan 05 '15 at 05:23
1

That came from the function docs. An old version is online. We should make them auto generate upon release: http://www.idris-lang.org/docs/prelude_doc/docs/[builtins].html#= – Brian McKenna Jan 05 '15 at 12:32

Using heterogenous equality with =

1 Answers1

Linked