[Git][ghc/ghc][wip/T18998] Unfortunate dirty hack to overcome #18998.

[Richard Eisenberg]

Richard Eisenberg pushed to branch wip/T18998 at Glasgow Haskell Compiler / GHC


Commits:
c73a55fd by Richard Eisenberg at 2020-12-11T11:14:08-05:00
Unfortunate dirty hack to overcome #18998.

See commentary in tcCheckUsage.

Close #18998.

Test case: typecheck/should_compile/T18998

- - - - -


3 changed files:

- compiler/GHC/Tc/Utils/Env.hs
- + testsuite/tests/typecheck/should_compile/T18998.hs
- testsuite/tests/typecheck/should_compile/all.T


Changes:

=====================================
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,40 @@ 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' <- 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


=====================================
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


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -737,3 +737,4 @@ test('InstanceGivenOverlap2', normal, compile, [''])
 test('LocalGivenEqs', normal, compile, [''])
 test('LocalGivenEqs2', normal, compile, [''])
 test('T18891', normal, compile, [''])
+test('T18998', normal, compile, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73a55fdf63ed5fa31540d15275bdff03c872f70

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73a55fdf63ed5fa31540d15275bdff03c872f70
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201211/2dac1d01/attachment-0001.html>