idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-08-17 17:20:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1275 from edwinb/fix1274

Browse Source 
Use correct multiplicity in scope of lets
This commit is contained in:
Edwin Brady 2021-04-04 19:17:36 +01:00 committed by GitHub
commit 7714bdf3fd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 15 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Core/LinearCheck.idr
View File

@ -291,6 +291,7 @@ mutual
if isErased rig_in
then erased
else top -- checking as if an inspectable run-time type
Let _ _ _ _ => rig_in
_ => if isErased rig_in
then erased
else linear

2
tests/Main.idr
View File

@ -126,7 +126,7 @@ idrisTestsRegression = MkTestPool []
"reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
"reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
"reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
"reg036", "reg037", "reg038"]
"reg036", "reg037", "reg038", "reg039"]
idrisTestsData : TestPool
idrisTestsData = MkTestPool []

2
tests/idris2/reg039/dupdup.idr Normal file
View File

@ -0,0 +1,2 @@
dupLinear : (1 x : a) -> (a, a)
dupLinear x = dup (let var = 22 in x)

8
tests/idris2/reg039/expected Normal file
View File

@ -0,0 +1,8 @@
1/1: Building dupdup (dupdup.idr)
Error: While processing right hand side of dupLinear. Trying to use linear name x in non-linear context.
dupdup.idr:2:24--2:32
1 | dupLinear : (1 x : a) -> (a, a)
2 | dupLinear x = dup (let var = 22 in x)
^^^^^^^^

3
tests/idris2/reg039/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-color --console-width 0 --check dupdup.idr
rm -rf build