[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:
eb5e4454 by Richard Eisenberg at 2020-12-11T15:13:42-05:00
Unfortunate dirty hack to overcome #18998.

See commentary in tcCheckUsage.

Close #18998.

Test case: typecheck/should_compile/T18998

- - - - -


4 changed files:

- compiler/GHC/Tc/Utils/Env.hs
- + testsuite/tests/typecheck/should_compile/T18998.hs
- + testsuite/tests/typecheck/should_compile/T18998b.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,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


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


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



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eb5e44547603513cad06ce6ef0392d15506f5f27
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/b3e0ccf2/attachment-0001.html>