Idris2
Idris2 copied to clipboard
idris-lang
Issue 2513 - handle erased, irrefutable lets
This PR addresses #2513 by adding a rig to ICase. It includes a test case named idris2/linear016.
It needs to be double checked by someone familiar with elaboration of case statements.
Note that it changes the shape of ICase, which could break some elaboration scripts (including the frex build). Should this be mentioned in the Changelog? What section / wording would be appropriate?
Question for the review: Does theRigCount on ICase need to be a Maybe RigCount?
We don't always know the ambient rigcount during desugaring, and maybe that means we need to keep guessing in those cases.
(But I haven't yet delved into the details of quantity checking, so maybe the elaborator can deal with that.)
I added tentative PR's for the two failing CI:
Both would need to be tweaked once this PR is merged, so we'll probably want to disable the frex CI for the duration of the merge into master, and disable the Elab utils CI for 1 day (until the nightly build updates).
Yeah, double check the Maybe thing. I thought about a Maybe, but saw the code for ILet in Binders.idr that it just multiplied the optionally supplied rig with ambient. I think is equivalent to having a Nothing, since RigW is a multiplicative identity. This is kinda how things work everwhere, right? If the user doesn't say anything it parses as RigW, but we pick up ambient. It doesn't look like we have Maybe RigCount anywhere else in the code base aside from two helper functions.
The other thing to review is that the code in Case.idr:checkCase and Binders.idr:checkLet is both complicated and almost identical, but ILet adds a {preciseInf := True} to the elabinfo in one spot and has an extra check instead of an error under the branchOne.
There is an additional test case from @ohad on discord that I'd like to look at later today. We solved the original error in that code with this PR, but it has another error in a slightly different spot now.
It's interesting that this fails:
data Foo : Bool -> Type where
MkInt : Int -> Foo True
MkString : String -> Foo False
blah : (0 f : Foo True) -> Int
blah f = let 0 (MkInt _) = f in 0
with
1/1: Building issue2513c (issue2513c.idr)
Error: While processing right hand side of blah. @-patterns only allowed in pattern clauses
issue2513c:7:14--7:29
3 | MkString : String -> Foo False
4 |
5 |
6 | blah : (0 f : Foo True) -> Int
7 | blah f = let 0 (MkInt _) = f in 0
But this works:
data Bar : Bool -> Type where
BarA : Bar True
BarB : Bar False
blah : (0 f : Bar True) -> Int
blah f = let 0 BarA = f in 0
as does the original
f : (0 x : (a,b)) -> Nat
f x =
let 0 (u,v) = x in
0
And this works too:
data Foo : Bool -> Type where
MkInt : Int -> Foo True
-- MkString : String -> Foo False
blah : (0 f : Foo True) -> Int
blah f = let 0 MkInt _ = f in 0
I think the BarA example shadows the constructor with a freshly bound variable.
Yeah, I wasn't used to binding capitalized names. With the parens, it fails:
data Bar : Bool -> Type where
BarA : Bar True
BarB : Bar False
blah : (0 f : Bar True) -> Int
blah f = let 0 (BarA) = f in 0
issue2513d:7:14--7:26:@-patterns only allowed in pattern clauses
Error: While processing right hand side of blah. @-patterns only allowed in pattern clauses
issue2513d:7:14--7:26
3 | BarA : Bar True
4 | BarB : Bar False
5 |
6 | blah : (0 _ : Bar True) -> Int
7 | blah f = let 0 (BarA) = f in 0
^^^^^^^^^^^^
So, with the example above, I'm getting these logs
LOG elab:10: Checking application of Main.case block in blah ($resolved2512) to [f@(BarA)]
Rig Rig1
Function type (0 f : (Main.Bar Prelude.Basics.True)) -> Int)
Expected app type Nothing
LOG elab.app.dot:50: Found Just 2 constructors for type: (Main.Bar Prelude.Basics.True)
LOG unify.meta:5: Adding new meta (Main.{f:831}, (issue2513d:8:14--8:26, Rig0))
LOG unify.meta:10: New meta type Main.{f:831}: (Main.Bar Prelude.Basics.True)
LOG elab:10: ...as: ?Main.{f:831}_[]
LOG elab:10: Now trying Main.{f:831} f@(.(f@(BarA))): (Main.Bar Prelude.Basics.True)
LOG elab.ambiguous:10: No ambiguity f@(.(f@(BarA)))
LOG elab.ambiguous:10: No ambiguity .(f@(BarA))
LOG elab.ambiguous:10: No ambiguity f@(BarA)
A dot is being constructed because It's finding two constructors - but only one of those constructors is valid because the type is Bar True:
https://github.com/idris-lang/Idris2/blob/128099fd47fc76d2796a9d19082dde4ab66580b8/src/TTImp/Elab/App.idr#L367-L380
So if it knew only one constructor was valid, this would be fine. But it'd still have the weird @ error if there happened to be two constructors. (Instead of a not covering error.)
Ok, I think there is a typo on App.idr:406, it's trying to rewrite a IAs, but stuffing the full term back inside instead of just that unification of the arg:
diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr
index cda4a587..71db9f83 100644
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@@ -403,7 +403,7 @@ mutual
Implicit _ _ => tm
IAs _ _ _ _ (IBindVar _ _) => tm
IAs _ _ _ _ (Implicit _ _) => tm
- IAs fc nameFC p t arg => IAs fc nameFC p t (IMustUnify fc ErasedArg tm)
+ IAs fc nameFC p t arg => IAs fc nameFC p t (IMustUnify fc ErasedArg arg)
_ => IMustUnify (getFC tm) ErasedArg tm
dotErased _ _ _ _ _ tm = pure tm
That resolves the @ error, but I still get:
Error: While processing right hand side of blah. Can't match on BarA (Erased argument).
I'll need to convince it that it doesn't need to dot that term.
I added tentative PR's for the two failing CI:
Both would need to be tweaked once this PR is merged, so we'll probably want to disable the frex CI for the duration of the merge into master, and disable the Elab utils CI for 1 day (until the nightly build updates).
I've checked in a change to temporarily disable these two tests. I also merged the latest from main.
Can we please summarise (perhaps in the original description) which cases work and which don't, and make sure there's a remaining issue for each unintended non-compiling case?
@ohad I think I might have that last case.
I took my example:
data Bar : Bool -> Type where
BarA : Bar True
BarB : Bar False
test5 : (0 _ : Bar True) -> Unit
test5 x = let 0 BarA = x
in ()
And ran both it and a manually desugared version with a lot of logging (and an additional temporary log statement), and compared the two. It turned out that the manually desugared version had the arg marked as safeErase, but Case.idr wasn't passing the safeErase info when creating the function for the case.
If I pass along the safeErase info, both my test case and the one you posted to discord work.
I was asked in Discord to report it here as it seems to be relevant to this PR.
In a code with a particular quantity in a pattern-matching let-binding, this quantity should affect all matched variables. Say, this code should not typecheck:
f : (Nat, Nat) -> Nat
f pair = let 0 (x, y) = pair
in x
For now, it typechecks both in main and in this PR.
Moreover, in the following code
record R where
constructor MkR
0 erased : Nat
1 linear : Nat
omega : Nat
r0 : R -> Nat
r0 r = let 0 MkR e l o = r in ?foo_0
-- I'd expect all `e`, `l` and `o` be 0
r1 : R -> Nat
r1 r = let 1 MkR e l o = r in ?foo_1
-- I'd expect `e` be `0` and `l` and `o` be `1`
rW : R -> Nat
rW r = let MkR e l o = r in ?foo_w
-- I'd expext `e` be `0`, `l` be `1` and `o` be omega
I'd expect the holes to have the following contexts:
0 o : Nat
0 l : Nat
0 e : Nat
r : R
------------------------------
foo_0 : Nat
1 o : Nat
1 l : Nat
0 e : Nat
r : R
------------------------------
foo_1 : Nat
o : Nat
1 l : Nat
0 e : Nat
r : R
------------------------------
foo_w : Nat
With compiler in main and this PR we have
o : Nat
l : Nat
0 e : Nat
r : R
------------------------------
foo_0 : Nat
o : Nat
l : Nat
0 e : Nat
r : R
------------------------------
foo_1 : Nat
o : Nat
l : Nat
0 e : Nat
r : R
------------------------------
foo_w : Nat
Thanks for finding those issues. I think I have the first one fixed locally and am looking into the others, but I'm not sure the last two are correctly stated:
1 o : Nat
1 l : Nat
0 e : Nat
r : R
------------------------------
foo_1 : Nat
o : Nat
l : Nat
0 e : Nat
r : R
------------------------------
foo_w : Nat
I don't fully grok the QTT stuff, but it appears that in Idris2, when you take apart a constructor with linear quantity, the stuff inside doesn't necessarily get the linear tag. I believe the case for r1 desugars to:
r1_case : (1 _: R) -> Nat
r1_case (MkR e l o) = ?foo_1
and at ?foo_1 the current Idris compiler reports:
Main> :t foo_1
o : Nat
1 l : Nat
0 e : Nat
------------------------------
foo_1 : Nat
And r2 would desugar to
r2_case : R -> Nat
r2_case (MkR e l o) = ?foo_w
for which the Idris compiler reports:
Main> :t foo_w
o : Nat
l : Nat
0 e : Nat
------------------------------
foo_w : Nat
Based on that I think we'd expect:
o : Nat
1 l : Nat
0 e : Nat
r : R
------------------------------
foo_1 : Nat
and
o : Nat
l : Nat
0 e : Nat
r : R
------------------------------
foo_w : Nat
I guess the last one makes sense, since you have ω copies of the argument, you can make ω copies of l, one from each of them. And in the previous one, you take apart one R, but it has ω copies of o inside it.
Let me know if I'm missing something here.
but I'm not sure the last two are correctly stated
First, I'm not sure let-binding with particular quantity has direct analogy in QTT itself, but unfortunately, I'm not competent enough to judge.
What you are saying, as far as I understand, is effectively "ignore any quantity except for 0 in let". I can't agree with this idea.
I understand (and my understanding can be wrong, of course) let q lhs = rhs as "pattern match rhs as lhs and limit all produced values to the quantity no more than q".
Say, you have let 1 x = y where y is omega. In this case despite y can have infinite copies, we are explicitly saying that we want x to have quantity of 1.
But take, say, a record with the only omega field, like Singleton type with Val constructor from base. To my view, nothing should change, i.e let 1 Val x = Val y should give the same result as let 1 x = y. But if I understand you correctly, you say that in the Singleton case we should get omega x when in the pure case we should have an x with quantity 1 (please, correct me if my understanding of your position is wrong).
But as far as I understand, having 0 in those lets makes them work the same even in your understanding. I'd consider this to be inconsistent.
I understand (and my understanding can be wrong, of course) let q lhs = rhs as "pattern match rhs as lhs and limit all produced values to the quantity no more than q".
That is maybe the root of our issue. The current implementation in this PR is that let q lhs = rhs means "pattern match rhs as lhs at quantity q". Given the current interpretation, I wonder if it should accept let 1 MkR e l o, given that it's being interpreted as let 1 (MkR e l o).
With the current interpretation, the object you're scrutinizing (rhs) would be observed at quantity q (like passing to a function as a quantity q argument). Assuming the Singleton case that you mentioned, it's like passing rhs to the function:
blah : (1 _ : Singleton a) -> SomeType
blah (Val x) = ...
(a let that pattern matches turns into a case, which turns into a function, so this essentially is the desugaring).
I wasn't suggesting that we ignore 1 in let (although the current PR lets Rig1 follow the existing code path), but rather that we treat it as a match of the whole scrutinee at linear quantity. (I.e. let 1 (Val x) = Val y in ...) In your test case, a 1 on the R times a 1 on the l gives us a 1. But a 1 on the R times a ω on the o gives us ω.
(You probably know the stuff below, but just summarizing how I understand linear to work.)
Looking at functions of a linear Singleton if we match with a linear quantity:
import Data.Singleton
foo : (1 _ : Singleton a) -> Nat
foo (Val x) = ?hole
we get:
Main> :t hole
x : a
0 a : a
------------------------------
hole : Nat
The Val x has quantity 1, but if we take it apart we have a quantity ω x inside. We're taking it apart once, to get the x, of which there are ω quantity. We end up with 1 • ω = ω of them.
Likewise, if we have a singleton with a linear field:
data Bar : Type -> Type where
MkBar : (1 _ : a) -> Bar a
bar : Bar a -> Nat
bar (MkBar x) = ?hole2
then we're taking apart ω copies of a Bar which has a linear x inside, and we get ω•1 = ω of them.
Main> :t hole2
0 a : Type
x : a
------------------------------
hole2 : Nat
I've run through all of the combinations of variable quantity and case quantity. To the cases described above, I added ones where the variable was linear, but scrutinized at various quantities.
There was an interesting case where you've got a linear variable and explicitly say you want to scrutinize it at Rig0. For that case, I left the linear variable unused, so the case body can have it. So in:
r10 : (1 _ : R) -> R
r10 r = let 0 (MkR e l o) = r in ?foo_10
The match is irrefutable, and the user says "I want to match this at level 0, without using the variable". The match happens (at quantity 0) and the variable is linearly available in ?foo_10:
1 r : R
0 o : Nat
0 l : Nat
0 e : Nat
------------------------------
foo_10 : R
Under the hood, we've got one argument to pass in the scrutinee (along with args for the rest of the environment) and another for the match:
LOG quantity:5: New type of Main.case block in r10: (1 r : Main.R) -> (0 {scr:1089} : Main.R) -> Main.R))
The extra argument also happens when we scrutinize an ω variable at 0 - we want the original variable to be available at full quantity inside the case block, but we want the match to happen at 0. So I'm setting splitOn to Nothing in those cases, and the scrutinee gets its own pi binding. So
rw0 : R -> Nat
rw0 r = let 0 (MkR e l o) = r in ?foo_w0
ends up as
LOG quantity:5: New type of Main.case block in rw0: (r : Main.R) -> (0 {scr:1052} : Main.R) -> Prelude.Types.Nat))
Also it currently requires the user to be explicit (let 0 ...) when they want to match a Rig0 variable within a RigW context:
failing "r is not accessible in this context"
r0w : (0 _ : R) -> Nat
r0w r = let (MkR e l o) = r in ?foo_0w
I think we'll want to add a count to the case statement in the surface syntax (PCase). Should I do this here or save it for a separate PR? I'd thinking something along the lines of case 0 x of ....
Should I update the description at the top to more concisely state what is now in the PR?
The current state of this PR is:
Changes let to interpret capitalized names as data constructors.
So let Just a = x in ... now matches against Just a instead of defining a function Just.
Allows users to match irrefutable patterns by adding a 0 to a pattern matching let statement.
So this is now accepted by the compiler:
data Bar : Bool -> Type where
BarA : Bar True
BarB : Bar False
test : (0 _ : Bar True) -> Unit
test x = let 0 BarA = x in ()
Note that if you explicitly match a linear variable at count 0, it will not be used and will still be linear in the let body.
Similarly, if you explicitly scrutinize a quantity ω variable at quantity 0, the original variable is still in scope at its original quantity.
Allows users to match irrefutable patterns by adding a 0 to a pattern matching lambda.
Matching at quantity 0 is extended to lambdas too:
test : (0 _ : (a,b)) -> Nat
test = \ 0 (u,v) => 1
Allows users to match an expression as linear by providing a 1 in the let statement.
This is like passing the scrutinee into a function at quantity 1, so
record R where
constructor MkR
0 erased : Nat
1 linear : Nat
omega : Nat
rw1 : R -> Nat
rw1 r = let 1 MkR e l o = r in ?hole
will show the following at ?hole
r : R
o : Nat
1 l : Nat
0 e : Nat
------------------------------
foo_w1 : Nat
The quantities for e,l,o are the same as they are in:
foo_w1_case : (1 _ : R) -> Nat
foo_w1_case (MkR e l o) = ?hole
Adds a RigCount to ICase
There is now a RigCount on ICase to carry the count from the let. The case will scrutinize at that count. This will require slight changes to some elaboration code (particularly the elab-util and frex).
This PR appears to be stalled, I'm not sure what it was waiting on (maybe further review).
If there is interest, I can rebase this and update to work with the latest code. But it might be prudent to wait until new core lands and redo any bits that are still relevant. I'm expecting the case elaboration code will change in that process.
Yeah I'm afraid this will conflict hard with the new core. And so given the merge strategy edwin is planning to use (basically: overwrite current idris2 with his fork), we would just end up losing this work. So I'd rather we wait for the new core.
I'm going to close this PR. We still have #2535 for the underlying issue, and I'll hold onto the tests. When new-core lands, we can see what it hasn't solved already and give it another go. I believe new core will be carrying more information that may make this this a bit easier and cleaner.