src/Idris/Elab/Interface.hs:(274,5)-(275,62): Non-exhaustive patterns in function getMName

[stephen-smith]

Please attach complete source files that exhibit the issue in addition to quoting from them here.

Steps to Reproduce

interface Queue (q : Type -> Type) where
  ||| An empty queue
  Empty : q a
  ||| Is the queue empty?
  IsEmpty : q a -> Bool
  ||| Enqueue a item
  Snoc : q a -> a -> q a
  ||| View the first item in the queue.  UNSAFE; Queue must not be empty.
  Head : q a -> a
  ||| Dequeue the first item from the queue.  UNSAFE: Queue must not be empty.
  Tail : q a -> q a
  ||| Proof that two queues contain the same items in the same order
  data QEqv : q a -> q a -> Type where
    Empties : .IsEmpty qx = True -> .IsEmpty qy = True
           -> QEqv impl qx qy
    Snocs : .IsEmpty qx = False -> .IsEmpty qy = False
         -> .Head qx = Head qy -> .QEqv (Tail qx) (Tail qy)
         -> QEqv qx qy

Expected Behavior

• Not an internal error
• Warning about associated types not working (?)

Observed Behavior

• If this is the only file being loaded, executable crashes.
• If this file is being type checked as a dependency / import, message (title) is printed, but REPL stays up, presumably using the old module.

[stephen-smith]

Attaching file as it exists today. Will work on min-repo.

Queue.idr.txt

---

Motivation. I'm trying to implement and prove correct the queue implementations in the Okasaki book. The Queue typeclass is mostly from them. However, I have an add-on VerifiedQueue typeclass, and one of the proofs in it need to mention the "queue-equivalence" of two values (Not value equality, that's too strong for all but a trvial implementation). I'm having trouble consistently referring to the same typeclass instance throughout QEqv and VerifiedQueue, and my latest attempt was to try and push QEqv into the Queue typeclass, resulting in this executable crash.

[stephen-smith]

Minimum reproduction

• Removing IsEmpty entirely results in a correct error message.
• Changing the type of IsEmpty to Bool or something that doesn't refer to q results in a correct error message.
• Removing the explicit type on q, letting Idris infer Type, and correcting the IsEmpty signature to be acceptable results in a correct error message.

Correct error message: Data definitions not allowed in an interface declaration.

[ahmadsalim]

@stephen-smith Thank you for reporting the error.