Missing functionality: impossibility assertions in pattern-matching anonymous functions

[vfrinken]

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!

Steps to Reproduce

import Decidable.Equality

data MyDATA = ABC | DEF

DecEq MyDATA where
  decEq ABC ABC = Yes Refl
  decEq ABC DEF = No (\Refl impossible)
  decEq DEF ABC = No (\Refl impossible)
  decEq DEF DEF = Yes Refl

Expected Behavior

type checking without problems Idris: File loaded successfully like Idris 1

Observed Behavior

Parse error: Not the end of a block entry (next tokens: [symbol (, symbol \, identifier Refl, impossible, symbol ), identifier decEq, identifier DEF, identifier ABC, symbol =, identifier No])

[ohad]

I think this is because the impossible on a pattern match in an anonymous function is not yet implemented.

If you're blocked on this, here's a work-around:

import Decidable.Equality

data MyDATA = ABC | DEF

DecEq MyDATA where
  decEq ABC ABC = Yes Refl
  decEq ABC DEF = No $ \case Refl impossible
  decEq DEF ABC = No $ \case Refl impossible
  decEq DEF DEF = Yes Refl

[gallais]

Worth noting we have lambda-case thanks to #244

[ohad]

Thanks!

I guess we should decide on whether this is a missing feature, or \case is the way to go.

[jfdm]

I would argue that lambda case is a good way to go. Especially, if it is well documented.