[ fix ] Fix pattern match issue with function application in Refl

[dunhamsteve]

Description

In discord @ohad reported a unification error where a function was being replaced by an application of the same function at type level. A test case that demonstrates the issue is included below. The root cause was that when a fx = f x was matched, the implicit argument fx in the spine was turned into fx@(f x). When this was later processed in mkPat in CaseBuilder.idr, the spine was being collected, but inadvertently dropped, so the resulting pattern looked like fx@f and fx was later substituted for f in a function call (note that they have completely different types).

The fix is to check for a non-empty spine and fallback to PUnmatchable if it's not empty. This results in a pattern that is dotted and includes the arguments: f@(.(f x)).

Consider:

import Data.Vect

bar : (f : List a -> Nat) -> (xs : List a) -> Nat
bar f xs = f xs

foo : (f : List a -> Nat) -> (xs : List a) -> (0 _ : fx = f xs) -> Nat
foo f xs Refl = bar f xs

blah : (xs : List a) -> Vect (foo List.length xs Refl) ()
blah xs = replicate (length xs) ()

If we comment out blah to get it to compile and look at :di foo in the current version of Idris:

Main.foo
Arguments [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]
Compile time tree: bar {arg:0} {arg:3}
Erasable args: [0, 1, 4]
Detaggable arg types: [4]
Inferrable args: [1]
Compiled: \ {arg:2}, {arg:3} => Main.bar {arg:2} {arg:3}
Refers to: Main.bar
Refers to (runtime): Main.bar
Flags: covering
Size change: Main.bar: [Just (1, Same), Just (2, Same), Just (3, Same)]

The compile time tree is passing arg:0 to bar, which is the wrong type. The compiled tree correctly passes arg:2.

Before this change, the code above failed to typecheck with:

1/1: Building LocalArgs (LocalArgs.idr)
Error: While processing right hand side of blah. When unifying:
    length xs xs
and:
    length xs

LocalArgs:11:11--11:35
 07 | foo : (f : List a -> Nat) -> (xs : List a) -> (0 _ : fx = f xs) -> Nat
 08 | foo f xs Refl = bar f xs
 09 | 
 10 | blah : (xs : List a) -> Vect (foo List.length xs Refl) ()
 11 | blah xs = replicate (length xs) ()
                ^^^^^^^^^^^^^^^^^^^^^^^^

After this change the file typechecks.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[dunhamsteve]

The tests chez007 and node007 are failing. The way in which they are failing is concerning (a pattern var is leaking), but I'm also wondering about those tests.

The issue is:

descFn ((x : Nat) -> b) = descNat (b Z)

which seems a little sketchy. In an actual type declaration, the corresponding type would read (x : Nat) -> b x. Looking at (x : Nat) -> b, I'd expect b : Type, and a type checking failure on b Z. But when case tree sees it, b is applied to a phantom argument, and the new code is rejecting it because it's a match against an App with a variable at the head.

[dunhamsteve]

I've gotten chez007 / node007 to pass by allowing a non-empty, but unmatchable spine. (Matching current behavior.)

But the existing behavior in chez007 still seems weird to me. On the LHS b looks like a Type and on the RHS, it looks like a Nat -> Type. (Essentially, (x : Nat) -> b on the LHS appears to b parsed as (x : Nat) -> b x:

descFn : (x : Type) -> String
descFn ((x : Nat) -> b) = descNat (b Z)
descFn (a -> b) = "Function on " ++ desc a
descFn x = desc x

[gallais]

Unfortunately it's the way it is. I agree it's confusing but currently all matches on -> are dependent
no matter how you write them.

[gallais]

I have found a regression, cf. test case.

[dunhamsteve]

To fix that regression, I tightened up the cases when this change is applied.

I don't know what (x : Type) -> x is supposed to mean. If it's interpreted literally, it would be something like Π x : Type . x, which I believe is uninhabited (given a type, it would return an instance, which is kinda tough for Void). Above, we interpret (x : Nat) -> b as Π x : Nat . b x, which might suggest (x : Type) -> x would be Π x : Type. x x. But that doesn't type check. It actually ended up compiling to a pattern Type -> .([__])) with the old code and with my most recent change, so I think it matches any function type Type -> a.

[dunhamsteve]

Build failed because main is failing.

[dunhamsteve]

There was an odd failure in the windows build, so I merged main to trigger another build. (Is there an easier way to retrigger CI on a branch?)

[dunhamsteve]

Windows test from a previous check-in is failing. I think it's due to not having error handling on the getLines function (and it's returning two random values subtracted). I've added the error handling code, but have to test it in CI.

[gallais]

It feels like we are piling hacks on top of hacks. I think what we need
here is a story of pattern-matching where we can talk about locally
bound variables like we have in TypOS (that pattern bind a body with
an extra x in scope which is exactly what we need for (x : _) -> body).

In the meantime I will merge this because the situation is already broken
IMO.