Unfortunate dirty hack to overcome #18998.

See commentary in tcCheckUsage.

Close #18998.

Test case: typecheck/should_compile/T18998

3 files changed, 44 insertions, 0 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T18998.hs b/testsuite/tests/typecheck/should_compile/T18998.hs
new file mode 100644
index 0000000000..25571bae30
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18998.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE LinearTypes, GADTs, DataKinds, KindSignatures #-}
+
+-- this caused a TcLevel assertion failure
+
+module T18998 where
+
+import GHC.Types
+import GHC.TypeLits
+
+data Id :: Nat -> Type -> Type where
+  MkId :: a %1-> Id 0 a
+
+f :: a %1-> Id n a -> Id n a
+f a (MkId _) = MkId a
diff --git a/testsuite/tests/typecheck/should_compile/T18998b.hs b/testsuite/tests/typecheck/should_compile/T18998b.hs
new file mode 100644
index 0000000000..d30a8fdba8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18998b.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables, LinearTypes, DataKinds, TypeOperators, GADTs,
+             PolyKinds, ConstraintKinds, TypeApplications #-}
+
+module T18998b where
+
+import GHC.TypeLits
+import Data.Kind
+import Unsafe.Coerce
+
+data Dict :: Constraint -> Type where
+  Dict :: c => Dict c
+knowPred :: Dict (KnownNat (n+1)) -> Dict (KnownNat n)
+knowPred Dict = unsafeCoerce (Dict :: Dict ())
+data NList :: Nat -> Type -> Type where
+  Nil :: NList 0 a
+  Cons :: a %1-> NList n a %1-> NList (n+1) a
+-- Alright, this breaks linearity for some unknown reason
+
+snoc :: forall n a. KnownNat n => a %1-> NList n a %1-> NList (n+1) a
+snoc a Nil = Cons a Nil
+snoc a (Cons x (xs :: NList n' a)) = case knowPred (Dict :: Dict (KnownNat n)) of
+   Dict -> Cons x (snoc a xs)
+-- This works fine
+
+snoc' :: forall n a. a %1-> NList n a %1-> NList (n+1) a
+snoc' a Nil = Cons a Nil
+snoc' a (Cons x xs) = Cons x (snoc' a xs)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 344b4394a9..f76741a447 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -749,3 +749,6 @@ test('TyAppPat_UniversalMulti2', normal, compile, [''])
 test('TyAppPat_UniversalMulti3', normal, compile, [''])
 test('TyAppPat_UniversalNested', normal, compile, [''])
 test('TyAppPat_Wildcard', normal, compile, [''])
+
+test('T18998', normal, compile, [''])
+test('T18998b', normal, compile, [''])