Unexpected "Trying to use linear name in non-linear context" when pattern matching inside the type

[buzden]

Steps to Reproduce

Consider a simple dependently typed function:

f1 : (n : Nat) -> Vect n Nat -> Vect (S n) Nat
f1 a b = a :: b

No problem. For some reason, one may want to have a match in side the type:

f2 : (n : Nat) -> case n of
  k => Vect k Nat -> Vect (S k) Nat
f2 a b = a :: b

No problem too. But here the match is just an introduction a new synonymous name, is does not do anything.

But as soon as you do the actual pattern match, you have problems:

f3 : (n : Nat) -> case n of
  Z => Vect Z Nat -> Vect (S Z) Nat
  (S k) => Vect (S k) Nat -> Vect (S (S k)) Nat
f3 Z b = a :: b
f3 (S a) b = a :: b

The single match alternative does the same thing:

f4 : (n : (Nat, Nat)) -> case n of
  (x, y) => Vect x Nat -> Vect (S x) Nat
f4 (_, a) b = a :: b

Expected Behavior

Typechecks well.

Observed Behavior

Error: While processing right hand side of f3. Trying to use linear name b in non-linear context.

.../SuspiciouslyLinear.idr:13:15--13:16
    |
 13 | f3 Z b = a :: b
    |               ^

Error: While processing right hand side of f4. Trying to use linear name b in non-linear context.

.../SuspiciouslyLinear.idr:18:20--18:21
    |
 18 | f4 (_, a) b = a :: b
    |                    ^

The problem suspiciously resembles #586 but seems to have nothing with mutual declarations.

[donovancrichton]

I tried the following and it type checks just fine:

f3 : (n : Nat) -> case n of
  Z => Vect Z Nat -> Vect (S Z) Nat
  (S k) => Vect (S k) Nat -> Vect (S (S k)) Nat
f3 Z = \b => Z :: b
f3 (S a) = \b => a :: b

Maybe we need a better error around why we can't bring in the first argument of the return function on the LHS?

[gallais]

I got bitten by this recently while trying to use a record update { f := True } st in the index of a type constructor (these update functions desugar to case blocks). My solution was to define toplevel setX functions but that's obviously a bit annoying.

[mjustus]

Here is what goes wrong: when checkAppWith' encounters a function type ty that doesn't have pi-shape, it constructs a type Bind fc argn (Pi fc top Explicit argTy) (weaken retTy), where argTy and retTy are fresh meta-variables. It then checks the function argument in question against meta-variable argTy using the ambient quantity rig.

https://github.com/idris-lang/Idris2/blob/572a4c74d6b79a79bc028f5bad93177b7103a731/src/TTImp/Elab/App.idr#L712-L725

This is wrong, of course: at this point the quantity annotation on the pi-type is some unknown quantity rigb (not top). The argument should be checked at rig |*| rigb.

This incorrect quantity gets propagated to the point where we bind the pattern variable

https://github.com/idris-lang/Idris2/blob/572a4c74d6b79a79bc028f5bad93177b7103a731/src/TTImp/Elab/ImplicitBind.idr#L456-L457

Concretely, the pattern f4 (_, a) b is checked at (default) quantity Rig1. Idris first looks up the type of f4 : (n : (Nat, Nat)) -> sc and then checks the pattern arguments against this type proceeding right to left. This involves introducing a meta-variable (which will later be instantiated with (_, a)), applying it to sc and then checking whether b is a valid argument to the resulting type

https://github.com/idris-lang/Idris2/blob/572a4c74d6b79a79bc028f5bad93177b7103a731/src/TTImp/Elab/App.idr#L469-L475

However, evaluation of sc applied to a meta-variables gets stuck so we end in the situation described above. We continue checking pattern b at quantity Rig1, which we then use to bind the pattern variable in the elaborator state.