Unfortunate dirty hack to overcome #18998.wip/T18998

See commentary in tcCheckUsage.

Close #18998.

Test case: typecheck/should_compile/T18998

4 files changed, 77 insertions, 1 deletions

diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 199fb57cc6..1b13d82869 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -102,6 +102,7 @@ import GHC.Core.ConLike
 import GHC.Core.TyCon
 import GHC.Core.Type
 import GHC.Core.Coercion.Axiom
+import GHC.Core.Coercion
 import GHC.Core.Class
 
 import GHC.Unit.Module
@@ -663,10 +664,41 @@ tcCheckUsage name id_mult thing_inside
            ; wrapper <- case actual_u of
                Bottom -> return idHsWrapper
                Zero     -> tcSubMult (UsageEnvironmentOf name) Many id_mult
-               MUsage m -> tcSubMult (UsageEnvironmentOf name) m id_mult
+               MUsage m -> do { m <- zonkTcType m
+                              ; m <- promote_mult m
+                              ; tcSubMult (UsageEnvironmentOf name) m id_mult }
            ; tcEmitBindingUsage (deleteUE uenv name)
            ; return wrapper }
 
+    -- This is gross. The problem is in test case typecheck/should_compile/T18998:
+    --   f :: a %1-> Id n a -> Id n a
+    --   f x (MkId _) = MkId x
+    -- where MkId is a GADT constructor. Multiplicity polymorphism of constructors
+    -- invents a new multiplicity variable p[2] for the application MkId x. This
+    -- variable is at level 2, bumped because of the GADT pattern-match (MkId _).
+    -- We eventually unify the variable with One, due to the call to tcSubMult in
+    -- tcCheckUsage. But by then, we're at TcLevel 1, and so the level-check
+    -- fails.
+    --
+    -- What to do? If we did inference "for real", the sub-multiplicity constraint
+    -- would end up in the implication of the GADT pattern-match, and all would
+    -- be well. But we don't have a real sub-multiplicity constraint to put in
+    -- the implication. (Multiplicity inference works outside the usual generate-
+    -- constraints-and-solve scheme.) Here, where the multiplicity arrives, we
+    -- must promote all multiplicity variables to reflect this outer TcLevel.
+    -- It's reminiscent of floating a constraint, really, so promotion is
+    -- appropriate. The promoteTcType function works only on types of kind TYPE rr,
+    -- so we can't use it here. Thus, this dirtiness.
+    --
+    -- It works nicely in practice.
+    (promote_mult, _, _, _) = mapTyCo mapper
+    mapper = TyCoMapper { tcm_tyvar = \ () tv -> do { _ <- promoteTyVar tv
+                                                    ; zonkTcTyVar tv }
+                        , tcm_covar = \ () cv -> return (mkCoVarCo cv)
+                        , tcm_hole  = \ () h  -> return (mkHoleCo h)
+                        , tcm_tycobinder = \ () tcv _flag -> return ((), tcv)
+                        , tcm_tycon = return }
+
 {- *********************************************************************
 *                                                                      *
              The TcBinderStack
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, [''])