[Git][ghc/ghc][wip/T18998] Unfortunate dirty hack to overcome #18998.
Richard Eisenberg
gitlab at gitlab.haskell.org
Fri Dec 11 04:07:05 UTC 2020
Richard Eisenberg pushed to branch wip/T18998 at Glasgow Haskell Compiler / GHC
Commits:
d1998b7f by Richard Eisenberg at 2020-12-10T23:06:51-05:00
Unfortunate dirty hack to overcome #18998.
See commentary in tcCollectingUsage, which had to move
modules to avoid import loops.
Close #18998.
Test case: typecheck/should_compile/T18998
- - - - -
7 changed files:
- compiler/GHC/Core/UsageEnv.hs
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Types/Name/Env.hs
- + testsuite/tests/typecheck/should_compile/T18998.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/UsageEnv.hs
=====================================
@@ -12,6 +12,7 @@ module GHC.Core.UsageEnv
, supUEs
, unitUE
, zeroUE
+ , nonDetMapUEM
) where
import Data.Foldable
@@ -52,7 +53,9 @@ scaleUsage x Bottom = MUsage x
scaleUsage x (MUsage y) = MUsage $ mkMultMul x y
-- For now, we use extra multiplicity Bottom for empty case.
-data UsageEnv = UsageEnv (NameEnv Mult) Bool
+data UsageEnv
+ = UsageEnv (NameEnv Mult) -- ^ mapping from names to their multiplicities
+ Bool -- ^ True <=> this is a bottom 'UsageEnv'; used for empty case
unitUE :: NamedThing n => n -> Mult -> UsageEnv
unitUE x w = UsageEnv (unitNameEnv (getName x) w) False
@@ -100,3 +103,10 @@ lookupUE (UsageEnv e has_bottom) x =
instance Outputable UsageEnv where
ppr (UsageEnv ne b) = text "UsageEnv:" <+> ppr ne <+> ppr b
+
+-- | Perform a applicative operation on all the 'Mult's in a 'UsageEnv'.
+-- The operation should *not* care about the order in which the
+-- environment is traversed.
+nonDetMapUEM :: Applicative m => (Mult -> m Mult) -> UsageEnv -> m UsageEnv
+nonDetMapUEM f (UsageEnv env is_bottom)
+ = UsageEnv <$> nonDetTraverseNameEnv f env <*> pure is_bottom
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -25,6 +25,7 @@ import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC )
import GHC.Builtin.Types (multiplicityTy)
import GHC.Tc.Gen.Head
import GHC.Hs
+import GHC.Tc.Utils.Env ( tcScalingUsage )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.Instantiate
@@ -1087,5 +1088,3 @@ tcTagToEnum expr fun args app_res_ty res_ty
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-
-
=====================================
compiler/GHC/Tc/Utils/Env.hs
=====================================
@@ -47,6 +47,9 @@ module GHC.Tc.Utils.Env(
getTypeSigNames,
tcExtendRecEnv, -- For knot-tying
+ -- * Usage environment
+ tcCollectingUsage, tcScalingUsage, tcEmitBindingUsage,
+
-- Tidying
tcInitTidyEnv, tcInitOpenTidyEnv,
@@ -102,6 +105,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
@@ -137,6 +141,8 @@ import Data.IORef
import Data.List (intercalate)
import Control.Monad
+import GHC.Driver.Ppr
+
{- *********************************************************************
* *
An IO interface to looking up globals
@@ -667,6 +673,67 @@ tcCheckUsage name id_mult thing_inside
; tcEmitBindingUsage (deleteUE uenv name)
; return wrapper }
+-----------------------
+-- | @tcCollectingUsage thing_inside@ runs @thing_inside@ and returns the usage
+-- information which was collected as part of the execution of
+-- @thing_inside at . Careful: @tcCollectingUsage thing_inside@ itself does not
+-- report any usage information, it's up to the caller to incorporate the
+-- returned usage information into the larger context appropriately.
+tcCollectingUsage :: TcM a -> TcM (UsageEnv,a)
+tcCollectingUsage thing_inside
+ = do { env0 <- getLclEnv
+ ; local_usage_ref <- newTcRef zeroUE
+ ; let env1 = env0 { tcl_usage = local_usage_ref }
+ ; result <- setLclEnv env1 thing_inside
+ ; local_usage <- readTcRef local_usage_ref
+ ; promoted_usage <- nonDetMapUEM promote_mult local_usage
+ ; return (promoted_usage,result) }
+ where
+ -- 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 }
+
+-- | @tcScalingUsage mult thing_inside@ runs @thing_inside@ and scales all the
+-- usage information by @mult at .
+tcScalingUsage :: Mult -> TcM a -> TcM a
+tcScalingUsage mult thing_inside
+ = do { (usage, result) <- tcCollectingUsage thing_inside
+ ; traceTc "tcScalingUsage" (ppr mult)
+ ; tcEmitBindingUsage $ scaleUE mult usage
+ ; return result }
+
+tcEmitBindingUsage :: UsageEnv -> TcM ()
+tcEmitBindingUsage ue
+ = do { lcl_env <- getLclEnv
+ ; let usage = tcl_usage lcl_env
+ ; updTcRef usage (addUE ue) }
+
+
{- *********************************************************************
* *
The TcBinderStack
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -71,9 +71,6 @@ module GHC.Tc.Utils.Monad(
addMessages,
discardWarnings,
- -- * Usage environment
- tcCollectingUsage, tcScalingUsage, tcEmitBindingUsage,
-
-- * Shared error message stuff: renamer and typechecker
mkLongErrAt, mkErrDocAt, addLongErrAt, reportErrors, reportError,
reportWarning, recoverM, mapAndRecoverM, mapAndReportM, foldAndRecoverM,
@@ -1273,36 +1270,6 @@ captureConstraints thing_inside
Nothing -> do { emitConstraints lie; failM }
Just res -> return (res, lie) }
------------------------
--- | @tcCollectingUsage thing_inside@ runs @thing_inside@ and returns the usage
--- information which was collected as part of the execution of
--- @thing_inside at . Careful: @tcCollectingUsage thing_inside@ itself does not
--- report any usage information, it's up to the caller to incorporate the
--- returned usage information into the larger context appropriately.
-tcCollectingUsage :: TcM a -> TcM (UsageEnv,a)
-tcCollectingUsage thing_inside
- = do { env0 <- getLclEnv
- ; local_usage_ref <- newTcRef zeroUE
- ; let env1 = env0 { tcl_usage = local_usage_ref }
- ; result <- setLclEnv env1 thing_inside
- ; local_usage <- readTcRef local_usage_ref
- ; return (local_usage,result) }
-
--- | @tcScalingUsage mult thing_inside@ runs @thing_inside@ and scales all the
--- usage information by @mult at .
-tcScalingUsage :: Mult -> TcM a -> TcM a
-tcScalingUsage mult thing_inside
- = do { (usage, result) <- tcCollectingUsage thing_inside
- ; traceTc "tcScalingUsage" (ppr mult)
- ; tcEmitBindingUsage $ scaleUE mult usage
- ; return result }
-
-tcEmitBindingUsage :: UsageEnv -> TcM ()
-tcEmitBindingUsage ue
- = do { lcl_env <- getLclEnv
- ; let usage = tcl_usage lcl_env
- ; updTcRef usage (addUE ue) }
-
-----------------------
attemptM :: TcRn r -> TcRn (Maybe r)
-- (attemptM thing_inside) runs thing_inside
=====================================
compiler/GHC/Types/Name/Env.hs
=====================================
@@ -8,6 +8,7 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
module GHC.Types.Name.Env (
-- * Var, Id and TyVar environments (maps)
@@ -22,7 +23,7 @@ module GHC.Types.Name.Env (
filterNameEnv, anyNameEnv,
plusNameEnv, plusNameEnv_C, plusNameEnv_CD, plusNameEnv_CD2, alterNameEnv,
lookupNameEnv, lookupNameEnv_NF, delFromNameEnv, delListFromNameEnv,
- elemNameEnv, mapNameEnv, disjointNameEnv,
+ elemNameEnv, mapNameEnv, disjointNameEnv, nonDetTraverseNameEnv,
DNameEnv,
@@ -44,6 +45,7 @@ import GHC.Types.Name
import GHC.Types.Unique.FM
import GHC.Types.Unique.DFM
import GHC.Data.Maybe
+import Data.Coerce
{-
************************************************************************
@@ -120,6 +122,8 @@ filterNameEnv :: (elt -> Bool) -> NameEnv elt -> NameEnv elt
anyNameEnv :: (elt -> Bool) -> NameEnv elt -> Bool
mapNameEnv :: (elt1 -> elt2) -> NameEnv elt1 -> NameEnv elt2
disjointNameEnv :: NameEnv a -> NameEnv a -> Bool
+nonDetTraverseNameEnv :: forall f a b. Applicative f
+ => (a -> f b) -> NameEnv a -> f (NameEnv b)
nameEnvElts x = eltsUFM x
emptyNameEnv = emptyUFM
@@ -145,6 +149,7 @@ delListFromNameEnv x y = delListFromUFM x y
filterNameEnv x y = filterUFM x y
anyNameEnv f x = foldUFM ((||) . f) False x
disjointNameEnv x y = disjointUFM x y
+nonDetTraverseNameEnv f n = fmap coerce $ traverse @(NonDetUniqFM Name) f $ coerce n
lookupNameEnv_NF env n = expectJust "lookupNameEnv_NF" (lookupNameEnv env n)
=====================================
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/d1998b7ff0c590cee7ca80f0fe296aec3bece3bc
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d1998b7ff0c590cee7ca80f0fe296aec3bece3bc
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/20201210/816898cb/attachment-0001.html>
More information about the ghc-commits
mailing list