Search code examples
idrisexistential-type

Match on existentially hidden type index

I'd like to match on an 'existentially hidden' type index, in order to write an Eq instance:

module Test

import Data.Vect

data Meep : Type where
  Moop : {n:Nat} -> Vect n Int -> Meep

Eq Meep where
  (Moop {n1} v1) == (Moop {n2} v2) = False

Subsequently, I'd like to have a view into decEq n1 n2 to delegate to Eq (Vect n Int) or to return False.

But the above doesn't seem to work:

Type checking .\.\Test.idr
.\.\Test.idr:9:9:
When checking left hand side of Prelude.Interfaces.Test.Meep implementation of Prelude.Interfaces.Eq, method ==:
n1 is not an implicit argument of Test.Moop

What is the actual Idris way of doing this?

Solution

  • You can do it this way:

    Eq Meep where
  (Moop {n = n1} v1) == (Moop {n = n2} v2) with (decEq n1 n2)
    (Moop {n = n2} v1) == (Moop {n = n2} v2) | (Yes Refl) = v1 == v2
    (Moop {n = n1} v1) == (Moop {n = n2} v2) | (No contra) = False