Mismatching quantities should be an impossible case?

[jmanuel1]

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

shouldBeImpossible : (((x : a) -> b) === ((0 x : a) -> b)) -> a
shouldBeImpossible prf impossible

Expected Behavior

The impossible case is accepted because ((x : a) -> b) and (0 x : a) -> b have mismatched quantities.

Observed Behavior

There is a type-checking error on the second line: shouldBeImpossible prf is not a valid impossible case.

[gallais]

AFAIK MLTT is currently a valid model of Idris 2 via quantities erasure.

Adding anti-unifiability of pi types with different annotations on their domain would force all models to discriminate between quantities. That's something we may want but we should be aware of that change in the theory.

[jmanuel1]

If I understand what you're saying, the theory behind Idris 2 is such that terms in that theory cannot be something you wouldn't be able to write if you ignored quantities. And you need quantities to distinguish quantities, therefore you cannot show that a -> b and (0 _ : a) -> b are different from within Idris.

[spcfox]

In some cases Idris now accepts an impossible case with different quantities. Since the evaluation ignores quantity, this allows us to prove false:

import Data.Maybe

%default total

data ErasedBind : Type -> Type where
  Impossible : Void => ErasedBind a
  Erased     : forall b. ErasedBind ((0 x : a) -> b x)

f : forall b. ErasedBind ((x : a) -> b x) -> Void
f Impossible impossible

g : (a : Type) -> ErasedBind a -> Maybe Void
g (a -> b) e = Just (f e)
g _ _ = Nothing

boom : Void
boom = fromJust $ g ((0 _ : Int) -> Int) Erased

I think we should consider quantity when matching on arrows to fix this inconsistency. This should also be consistent with the impossible cases that this issue is about

---

Similar code can be written for dependent/non-dependent Pi-types:

data NonDependentBind : Type -> Type where
  Impossible   : Void => NonDependentBind a
  NonDependent : NonDependentBind (a -> b)

f : forall b. NonDependentBind ((x : a) -> b x) -> Void
f Impossible impossible

g : (a : Type) -> NonDependentBind a -> Maybe Void
g (a -> b) e = Just (f e)
g _ _ = Nothing

boom : Void
boom = fromJust $ g ({_ : Int} -> Int) NonDependent

If I understand correctly, with matching on arrow, the type is always considered dependent, so we can't match on the right-hand side.

---

This example needs an Impossible constructor so that Idris knows that the function has a definition and checks all other cases itself. The check for user-defined impossible cases is slightly different and they are not accepted.

[spcfox]

I will fix the current bug in the coverage checker that leads to the proof of false above. However, if we allow anti-unification for pi-types, then we can write a similar proof of false:

data ErasedBind : Type -> Type where
  Erased : forall b. ErasedBind ((0 x : a) -> b x)

f : forall b. ErasedBind ((x : a) -> b x) -> Void
f Erased impossible

g : (a : Type) -> ErasedBind a -> Maybe Void
g (a -> b) e = Just (f e)
g _ _ = Nothing

boom : Void
boom = fromJust $ g ((0 _ : Int) -> Int) Erased

To preserve consistency, I think we also need to change the pattern matching on the arrows.

[jmanuel1]

@spcfox You might also be interested in https://github.com/idris-lang/Idris2/issues/3544