diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 5609ed9b5..729e3991d 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -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 diff --git a/tests/Main.idr b/tests/Main.idr index ebd50f824..52af704c8 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -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 [] diff --git a/tests/idris2/reg039/dupdup.idr b/tests/idris2/reg039/dupdup.idr new file mode 100644 index 000000000..e59e506c2 --- /dev/null +++ b/tests/idris2/reg039/dupdup.idr @@ -0,0 +1,2 @@ +dupLinear : (1 x : a) -> (a, a) +dupLinear x = dup (let var = 22 in x) diff --git a/tests/idris2/reg039/expected b/tests/idris2/reg039/expected new file mode 100644 index 000000000..ecd17a34e --- /dev/null +++ b/tests/idris2/reg039/expected @@ -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) + ^^^^^^^^ + diff --git a/tests/idris2/reg039/run b/tests/idris2/reg039/run new file mode 100755 index 000000000..2e94425ac --- /dev/null +++ b/tests/idris2/reg039/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --check dupdup.idr + +rm -rf build