[Git][ghc/ghc][wip/T18412] Allow multiple case branches to have a higher rank type
Simon Peyton Jones
gitlab at gitlab.haskell.org
Tue Jul 14 14:24:00 UTC 2020
Simon Peyton Jones pushed to branch wip/T18412 at Glasgow Haskell Compiler / GHC
Commits:
a60e30e0 by Simon Peyton Jones at 2020-07-14T15:22:15+01:00
Allow multiple case branches to have a higher rank type
As #18412 points out, it should be OK for multiple case alternatives
to have a higher rank type, provided they are all the same.
This patch implements that change. It sweeps away
GHC.Tc.Gen.Match.tauifyMultipleBranches, and friends, replacing it
with an enhanced version of fillInferResult.
The basic change to fillInferResult is to permit the case in which
another case alternative has already filled in the result; and in
that case simply unify. It's very simple actually.
See the new Note [fillInferResult] in TcMType
Other refactoring:
- Move all the InferResult code to one place, in GHC.Tc.Utils.TcMType
(previously some of it was in Unify)
- Move tcInstType and friends from TcMType to Instantiate, where it
more properly belongs. (TCMType was getting very long.)
- - - - -
21 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/UsageEnv.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/TyCl/Class.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/simplCore/should_compile/T17901.stdout
- + testsuite/tests/typecheck/should_compile/T18412.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T10619.stderr
- testsuite/tests/typecheck/should_fail/VtaFail.stderr
- testsuite/tests/typecheck/should_fail/tcfail002.stderr
- testsuite/tests/typecheck/should_fail/tcfail104.stderr
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -19,7 +19,7 @@ Note [The Type-related module hierarchy]
-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK not-home #-}
-{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
+{-# LANGUAGE CPP, MultiWayIf, PatternSynonyms, BangPatterns, DeriveDataTypeable #-}
module GHC.Core.TyCo.Rep (
TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
@@ -2025,6 +2025,12 @@ GHC.Core.Multiplicity above this module.
-- | A shorthand for data with an attached 'Mult' element (the multiplicity).
data Scaled a = Scaled Mult a
deriving (Data.Data)
+ -- You might think that this would be a natural candiate for
+ -- Functor, Traversable but Krzysztof says (!3674) "it was too easy
+ -- to accidentally lift functions (substitutions, zonking etc.) from
+ -- Type -> Type to Scaled Type -> Scaled Type, ignoring
+ -- multiplicities and causing bugs". So we don't.
+
instance (Outputable a) => Outputable (Scaled a) where
ppr (Scaled _cnt t) = ppr t
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -48,7 +48,7 @@ module GHC.Core.Type (
mkSpecForAllTy, mkSpecForAllTys,
mkVisForAllTys, mkTyCoInvForAllTy,
mkInfForAllTy, mkInfForAllTys,
- splitForAllTys, splitSomeForAllTys,
+ splitForAllTys,
splitForAllTysReq, splitForAllTysInvis,
splitForAllVarBndrs,
splitForAllTy_maybe, splitForAllTy,
@@ -284,7 +284,7 @@ import GHC.Data.List.SetOps
import GHC.Types.Unique ( nonDetCmpUnique )
import GHC.Data.Maybe ( orElse, expectJust )
-import Data.Maybe ( isJust, mapMaybe )
+import Data.Maybe ( isJust )
import Control.Monad ( guard )
-- $type_classification
@@ -1526,46 +1526,34 @@ splitForAllTys ty = split ty ty []
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
--- | Like 'splitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
--- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
--- @argf_pred@ is a predicate over visibilities provided as an argument to this
--- function. Furthermore, each returned tyvar is annotated with its @argf at .
-splitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
+-- | Splits the longest initial sequence of ForAllTys' that satisfy
+-- @argf_pred@, returning the binders transformed by @argf_pred@
+splitSomeForAllTys :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type)
splitSomeForAllTys argf_pred ty = split ty ty []
where
- split _ (ForAllTy tvb@(Bndr _ argf) ty) tvs
- | argf_pred argf = split ty ty (tvb:tvs)
+ split _ (ForAllTy (Bndr tcv argf) ty) tvs
+ | Just argf' <- argf_pred argf = split ty ty (Bndr tcv argf' : tvs)
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
-- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Required' type
-- variable binders. Furthermore, each returned tyvar is annotated with '()'.
splitForAllTysReq :: Type -> ([ReqTVBinder], Type)
-splitForAllTysReq ty =
- let (all_bndrs, body) = splitSomeForAllTys isVisibleArgFlag ty
- req_bndrs = mapMaybe mk_req_bndr_maybe all_bndrs in
- ASSERT( req_bndrs `equalLength` all_bndrs )
- (req_bndrs, body)
+splitForAllTysReq ty = splitSomeForAllTys argf_pred ty
where
- mk_req_bndr_maybe :: TyCoVarBinder -> Maybe ReqTVBinder
- mk_req_bndr_maybe (Bndr tv argf) = case argf of
- Required -> Just $ Bndr tv ()
- Invisible _ -> Nothing
+ argf_pred :: ArgFlag -> Maybe ()
+ argf_pred Required = Just ()
+ argf_pred (Invisible {}) = Nothing
-- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Invisible' type
-- variable binders. Furthermore, each returned tyvar is annotated with its
-- 'Specificity'.
splitForAllTysInvis :: Type -> ([InvisTVBinder], Type)
-splitForAllTysInvis ty =
- let (all_bndrs, body) = splitSomeForAllTys isInvisibleArgFlag ty
- inv_bndrs = mapMaybe mk_inv_bndr_maybe all_bndrs in
- ASSERT( inv_bndrs `equalLength` all_bndrs )
- (inv_bndrs, body)
+splitForAllTysInvis ty = splitSomeForAllTys argf_pred ty
where
- mk_inv_bndr_maybe :: TyCoVarBinder -> Maybe InvisTVBinder
- mk_inv_bndr_maybe (Bndr tv argf) = case argf of
- Invisible s -> Just $ Bndr tv s
- Required -> Nothing
+ argf_pred :: ArgFlag -> Maybe Specificity
+ argf_pred Required = Nothing
+ argf_pred (Invisible spec) = Just spec
-- | Like splitForAllTys, but split only for tyvars.
-- This always succeeds, even if it returns only an empty list. Note that the
=====================================
compiler/GHC/Core/UsageEnv.hs
=====================================
@@ -1,7 +1,7 @@
{-# LANGUAGE ViewPatterns #-}
module GHC.Core.UsageEnv (UsageEnv, addUsage, scaleUsage, zeroUE,
lookupUE, scaleUE, deleteUE, addUE, Usage(..), unitUE,
- supUE, supUEs) where
+ bottomUE, supUE, supUEs) where
import Data.Foldable
import GHC.Prelude
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -591,10 +591,6 @@ tcExpr (HsCase x scrut matches) res_ty
tcExpr (HsIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if'
= do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
- ; res_ty <- tauifyExpType res_ty
- -- Just like Note [Case branches must never infer a non-tau type]
- -- in GHC.Tc.Gen.Match (See #10619)
-
; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty
; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty
; tcEmitBindingUsage (supUE u1 u2)
@@ -611,13 +607,7 @@ tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty
; return (HsIf x fun' pred' b1' b2') }
tcExpr (HsMultiIf _ alts) res_ty
- = do { res_ty <- if isSingleton alts
- then return res_ty
- else tauifyExpType res_ty
- -- Just like GHC.Tc.Gen.Match
- -- Note [Case branches must never infer a non-tau type]
-
- ; alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
+ = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
; res_ty <- readExpType res_ty
; return (HsMultiIf res_ty alts') }
where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -164,80 +164,47 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (mkCheckExpType res_ty)
match_ctxt = MC { mc_what = PatBindRhs,
mc_body = tcBody }
-{-
-************************************************************************
+{- *********************************************************************
* *
-\subsection{tcMatch}
+ tcMatch
* *
-************************************************************************
-
-Note [Case branches must never infer a non-tau type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
- case ... of
- ... -> \(x :: forall a. a -> a) -> x
- ... -> \y -> y
-
-Should that type-check? The problem is that, if we check the second branch
-first, then we'll get a type (b -> b) for the branches, which won't unify
-with the polytype in the first branch. If we check the first branch first,
-then everything is OK. This order-dependency is terrible. So we want only
-proper tau-types in branches (unless a sigma-type is pushed down).
-This is what expTypeToType ensures: it replaces an Infer with a fresh
-tau-type.
-
-An even trickier case looks like
-
- f x True = x undefined
- f x False = x ()
-
-Here, we see that the arguments must also be non-Infer. Thus, we must
-use expTypeToType on the output of matchExpectedFunTys, not the input.
-
-But we make a special case for a one-branch case. This is so that
-
- f = \(x :: forall a. a -> a) -> x
-
-still gets assigned a polytype.
--}
+********************************************************************* -}
--- | When the MatchGroup has multiple RHSs, convert an Infer ExpType in the
--- expected type into TauTvs.
--- See Note [Case branches must never infer a non-tau type]
-tauifyMultipleMatches :: [LMatch id body]
- -> [Scaled ExpType] -> TcM [Scaled ExpType]
-tauifyMultipleMatches group exp_tys
- | isSingletonMatchGroup group = return exp_tys
- | otherwise = mapM (\(Scaled m t) ->
- fmap (Scaled m) (tauifyExpType t)) exp_tys
- -- NB: In the empty-match case, this ensures we fill in the ExpType
+data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module
+ = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is
+ mc_body :: Located (body GhcRn) -- Type checker for a body of
+ -- an alternative
+ -> ExpRhoType
+ -> TcM (Located (body GhcTc)) }
-- | Type-check a MatchGroup.
tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body
-> [Scaled ExpSigmaType] -- Expected pattern types
- -> ExpRhoType -- Expected result-type of the Match.
+ -> ExpRhoType -- Expected result-type of the Match.
-> MatchGroup GhcRn (Located (body GhcRn))
-> TcM (MatchGroup GhcTc (Located (body GhcTc)))
-data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module
- = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is
- mc_body :: Located (body GhcRn) -- Type checker for a body of
- -- an alternative
- -> ExpRhoType
- -> TcM (Located (body GhcTc)) }
tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
, mg_origin = origin })
- = do { (Scaled _ rhs_ty):pat_tys <- tauifyMultipleMatches matches ((Scaled One rhs_ty):pat_tys) -- return type has implicitly multiplicity 1, it doesn't matter all that much in this case since it isn't used and is eliminated immediately.
- -- See Note [Case branches must never infer a non-tau type]
+ | null matches -- Deal with case e of {}
+ -- Since there are no branches, no one else will fill in rhs_ty
+ -- when in inference mode, so we must do it ourselves,
+ -- here, using expTypeToType
+ = do { tcEmitBindingUsage bottomUE
+ ; pat_tys <- mapM scaledExpTypeToType pat_tys
+ ; rhs_ty <- expTypeToType rhs_ty
+ ; return (MG { mg_alts = L l []
+ , mg_ext = MatchGroupTc pat_tys rhs_ty
+ , mg_origin = origin }) }
- ; umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
+ | otherwise
+ = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
; let (usages,matches') = unzip umatches
; tcEmitBindingUsage $ supUEs usages
- ; pat_tys <- mapM (\(Scaled m t) -> fmap (Scaled m) (readExpType t)) pat_tys
+ ; pat_tys <- mapM readScaledExpType pat_tys
; rhs_ty <- readExpType rhs_ty
- ; return (MG { mg_alts = L l matches'
- , mg_ext = MatchGroupTc pat_tys rhs_ty
+ ; return (MG { mg_alts = L l matches'
+ , mg_ext = MatchGroupTc pat_tys rhs_ty
, mg_origin = origin }) }
-------------
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -220,8 +220,9 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl
= do { (co, bndr_ty) <- case scaledThing exp_pat_ty of
Check pat_ty -> promoteTcType bind_lvl pat_ty
Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
- -- If we were under a constructor that bumped
- -- the level, we'd be in checking mode
+ -- If we were under a constructor that bumped the
+ -- level, we'd be in checking mode (see tcConArg)
+ -- hence this assertion
do { bndr_ty <- inferResultToType infer_res
; return (mkTcNomReflCo bndr_ty, bndr_ty) }
; let bndr_mult = scaledMult exp_pat_ty
@@ -629,10 +630,9 @@ There are two bits of rebindable syntax:
lit1_ty and lit2_ty could conceivably be different.
var_ty is the type inferred for x, the variable in the pattern.
-If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
-could conceivably be different specializations. But this is very much
-like the situation in Note [Case branches must be taus] in GHC.Tc.Gen.Match.
-So we tauify the pat_ty before proceeding.
+If the pushed-down pattern type isn't a tau-type, the two pat_ty's
+above could conceivably be different specializations. So we use
+expTypeToType on pat_ty before proceeding.
Note that we need to type-check the literal twice, because it is used
twice, and may be used at different types. The second HsOverLit stored in the
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -36,7 +36,7 @@ import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
-import GHC.Tc.Utils.Instantiate( topInstantiate )
+import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
import GHC.Tc.Utils.Env( tcLookupId )
import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
import GHC.Core.Type ( mkTyVarBinders )
@@ -488,7 +488,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
-- Instantiate a type signature; only used with plan InferGen
tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Set the binding site of the tyvars
- do { (tv_prs, theta, tau) <- tcInstTypeBndrs newMetaTyVarTyVars poly_id
+ do { (tv_prs, theta, tau) <- tcInstTypeBndrs poly_id
-- See Note [Pattern bindings and complete signatures]
; return (TISI { sig_inst_sig = sig
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -16,6 +16,7 @@ import GHC.Prelude
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Instantiate( tcInstType )
import GHC.Tc.Instance.Typeable
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
=====================================
compiler/GHC/Tc/Instance/Family.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Core.Coercion
import GHC.Tc.Types.Evidence
import GHC.Iface.Load
import GHC.Tc.Utils.Monad
+import GHC.Tc.Utils.Instantiate( freshenTyVarBndrs, freshenCoVarBndrsX )
import GHC.Types.SrcLoc as SrcLoc
import GHC.Core.TyCon
import GHC.Tc.Utils.TcType
@@ -35,7 +36,6 @@ import GHC.Data.Maybe
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr ( pprWithExplicitKindsWhen )
-import GHC.Tc.Utils.TcMType
import GHC.Types.Name
import GHC.Utils.Panic
import GHC.Types.Var.Set
=====================================
compiler/GHC/Tc/TyCl/Class.hs
=====================================
@@ -31,11 +31,12 @@ where
import GHC.Prelude
import GHC.Hs
-import GHC.Tc.Utils.Env
import GHC.Tc.Gen.Sig
import GHC.Tc.Types.Evidence ( idHsWrapper )
import GHC.Tc.Gen.Bind
+import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Unify
+import GHC.Tc.Utils.Instantiate( tcSuperSkolTyVars )
import GHC.Tc.Gen.HsType
import GHC.Tc.Utils.TcMType
import GHC.Core.Type ( piResultTys )
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -16,6 +16,12 @@ module GHC.Tc.Utils.Instantiate (
instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds,
+ tcInstType, tcInstTypeBndrs,
+ tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
+ tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
+
+ freshenTyVarBndrs, freshenCoVarBndrsX,
+
tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
newOverloadedLit, mkOverLit,
@@ -63,7 +69,7 @@ import GHC.Types.Id.Make( mkDictFunId )
import GHC.Core( Expr(..) ) -- For the Coercion constructor
import GHC.Types.Id
import GHC.Types.Name
-import GHC.Types.Var ( EvVar, tyVarName, VarBndr(..) )
+import GHC.Types.Var
import GHC.Core.DataCon
import GHC.Types.Var.Env
import GHC.Builtin.Names
@@ -74,7 +80,7 @@ import GHC.Utils.Outputable
import GHC.Types.Basic ( TypeOrKind(..) )
import qualified GHC.LanguageExtensions as LangExt
-import Data.List ( sortBy )
+import Data.List ( sortBy, mapAccumL )
import Control.Monad( unless )
import Data.Function ( on )
@@ -451,15 +457,192 @@ mkEqBoxTy co ty1 ty2
mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
where k = tcTypeKind ty1
-{-
-************************************************************************
+{- *********************************************************************
* *
- Literals
+ SkolemTvs (immutable)
* *
-************************************************************************
+********************************************************************* -}
+tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
+ -- ^ How to instantiate the type variables
+ -> Id -- ^ Type to instantiate
+ -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
+ -- (type vars, preds (incl equalities), rho)
+tcInstType inst_tyvars id
+ | null tyvars -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
+ = return ([], theta, tau)
+ | otherwise
+ = do { (subst, tyvars') <- inst_tyvars tyvars
+ ; let tv_prs = map tyVarName tyvars `zip` tyvars'
+ subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+ ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
+ where
+ (tyvars, rho) = tcSplitForAllTys (idType id)
+ (theta, tau) = tcSplitPhiTy rho
+
+tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
+ -- (type vars, preds (incl equalities), rho)
+-- Instantiate the binders of a type signature with TyVarTvs
+tcInstTypeBndrs id
+ | null tyvars -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
+ = return ([], theta, tau)
+ | otherwise
+ = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars
+ ; let tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars'
+ subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+ ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
+ where
+ (tyvars, rho) = splitForAllTysInvis (idType id)
+ (theta, tau) = tcSplitPhiTy rho
+
+ inst_invis_bndr :: TCvSubst -> InvisTVBinder
+ -> TcM (TCvSubst, InvisTVBinder)
+ inst_invis_bndr subst (Bndr tv spec)
+ = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
+ ; return (subst', Bndr tv' spec) }
+
+tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants.
+-- We could give them fresh names, but no need to do so
+tcSkolDFunType dfun
+ = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
+ ; return (map snd tv_prs, theta, tau) }
+
+tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
+-- Make skolem constants, but do *not* give them new names, as above
+-- Moreover, make them "super skolems"; see comments with superSkolemTv
+-- see Note [Kind substitution when instantiating]
+-- Precondition: tyvars should be ordered by scoping
+tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
+
+tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
+tcSuperSkolTyVar subst tv
+ = (extendTvSubstWithClone subst tv new_tv, new_tv)
+ where
+ kind = substTyUnchecked subst (tyVarKind tv)
+ new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
+
+-- | Given a list of @['TyVar']@, skolemize the type variables,
+-- returning a substitution mapping the original tyvars to the
+-- skolems, and the list of newly bound skolems.
+tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
+
+tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
+
+tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
+
+tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+-- See Note [Skolemising type variables]
+tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
+
+tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
+ -> TcM (TCvSubst, [TcTyVar])
+-- Skolemise one level deeper, hence pushTcLevel
+-- See Note [Skolemising type variables]
+tcInstSkolTyVarsPushLevel overlappable subst tvs
+ = do { tc_lvl <- getTcLevel
+ ; let pushed_lvl = pushTcLevel tc_lvl
+ ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
+
+tcInstSkolTyVarsAt :: TcLevel -> Bool
+ -> TCvSubst -> [TyVar]
+ -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsAt lvl overlappable subst tvs
+ = freshenTyCoVarsX new_skol_tv subst tvs
+ where
+ details = SkolemTv lvl overlappable
+ new_skol_tv name kind = mkTcTyVar name kind details
+
+------------------
+freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
+-- ^ Give fresh uniques to a bunch of TyVars, but they stay
+-- as TyVars, rather than becoming TcTyVars
+-- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
+freshenTyVarBndrs = freshenTyCoVars mkTyVar
+
+freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
+-- ^ Give fresh uniques to a bunch of CoVars
+-- Used in "GHC.Tc.Instance.Family.newFamInst"
+freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
+
+------------------
+freshenTyCoVars :: (Name -> Kind -> TyCoVar)
+ -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
+freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
+
+freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
+ -> TCvSubst -> [TyCoVar]
+ -> TcM (TCvSubst, [TyCoVar])
+freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
+
+freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
+ -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
+-- This a complete freshening operation:
+-- the skolems have a fresh unique, and a location from the monad
+-- See Note [Skolemising type variables]
+freshenTyCoVarX mk_tcv subst tycovar
+ = do { loc <- getSrcSpanM
+ ; uniq <- newUnique
+ ; let old_name = tyVarName tycovar
+ new_name = mkInternalName uniq (getOccName old_name) loc
+ new_kind = substTyUnchecked subst (tyVarKind tycovar)
+ new_tcv = mk_tcv new_name new_kind
+ subst1 = extendTCvSubstWithClone subst tycovar new_tcv
+ ; return (subst1, new_tcv) }
+
+{- Note [Skolemising type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The tcInstSkolTyVars family of functions instantiate a list of TyVars
+to fresh skolem TcTyVars. Important notes:
+
+a) Level allocation. We generally skolemise /before/ calling
+ pushLevelAndCaptureConstraints. So we want their level to the level
+ of the soon-to-be-created implication, which has a level ONE HIGHER
+ than the current level. Hence the pushTcLevel. It feels like a
+ slight hack.
+
+b) The [TyVar] should be ordered (kind vars first)
+ See Note [Kind substitution when instantiating]
+
+c) It's a complete freshening operation: the skolems have a fresh
+ unique, and a location from the monad
+
+d) The resulting skolems are
+ non-overlappable for tcInstSkolTyVars,
+ but overlappable for tcInstSuperSkolTyVars
+ See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
+ of where this matters.
+
+Note [Kind substitution when instantiating]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we instantiate a bunch of kind and type variables, first we
+expect them to be topologically sorted.
+Then we have to instantiate the kind variables, build a substitution
+from old variables to the new variables, then instantiate the type
+variables substituting the original kind.
+
+Exemple: If we want to instantiate
+ [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
+we want
+ [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
+instead of the bogus
+ [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
-}
+{- *********************************************************************
+* *
+ Literals
+* *
+********************************************************************* -}
+
{-
In newOverloadedLit we convert directly to an Int or Integer if we
know that's what we want. This may save some time, by not
@@ -474,8 +657,6 @@ newOverloadedLit :: HsOverLit GhcRn
newOverloadedLit
lit@(OverLit { ol_val = val, ol_ext = rebindable }) res_ty
| not rebindable
- -- all built-in overloaded lits are tau-types, so we can just
- -- tauify the ExpType
= do { res_ty <- expTypeToType res_ty
; dflags <- getDynFlags
; let platform = targetPlatform dflags
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -31,15 +31,6 @@ module GHC.Tc.Utils.TcMType (
newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName,
isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar,
- --------------------------------
- -- Expected types
- ExpType(..), ExpSigmaType, ExpRhoType,
- mkCheckExpType,
- newInferExpType,
- readExpType, readExpType_maybe,
- expTypeToType, checkingExpType_maybe, checkingExpType,
- tauifyExpType, inferResultToType,
-
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
@@ -58,14 +49,18 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Instantiation
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
- newMetaTyVarTyVars, newMetaTyVarTyVarX,
+ newMetaTyVarTyVarX,
newTyVarTyVar, cloneTyVarTyVar,
newPatSigTyVar, newSkolemTyVar, newWildCardX,
- tcInstType, tcInstTypeBndrs,
- tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
- tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
- freshenTyVarBndrs, freshenCoVarBndrsX,
+ --------------------------------
+ -- Expected types
+ ExpType(..), ExpSigmaType, ExpRhoType,
+ mkCheckExpType, newInferExpType, tcInfer,
+ readExpType, readExpType_maybe, readScaledExpType,
+ expTypeToType, scaledExpTypeToType,
+ checkingExpType_maybe, checkingExpType,
+ inferResultToType, fillInferResult, promoteTcType,
--------------------------------
-- Zonking and tidying
@@ -99,6 +94,8 @@ module GHC.Tc.Utils.TcMType (
-- friends:
import GHC.Prelude
+import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} )
+
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Tc.Utils.TcType
@@ -133,7 +130,6 @@ import GHC.Types.Basic ( TypeOrKind(..) )
import Control.Monad
import GHC.Data.Maybe
-import Data.List ( mapAccumL )
import Control.Arrow ( second )
import qualified Data.Semigroup as Semi
@@ -387,16 +383,14 @@ checkCoercionHole cv co
| otherwise
= False
-{-
-************************************************************************
+{- **********************************************************************
*
- Expected types
+ ExpType functions
*
-************************************************************************
-
-Note [ExpType]
-~~~~~~~~~~~~~~
+********************************************************************** -}
+{- Note [ExpType]
+~~~~~~~~~~~~~~~~~
An ExpType is used as the "expected type" when type-checking an expression.
An ExpType can hold a "hole" that can be filled in by the type-checker.
This allows us to have one tcExpr that works in both checking mode and
@@ -426,14 +420,12 @@ Consider
This is a classic untouchable-variable / ambiguous GADT return type
scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
-And, because there is only one branch of the case, we won't trigger
-Note [Case branches must never infer a non-tau type] of GHC.Tc.Gen.Match.
We thus must track a TcLevel in an Inferring ExpType. If we try to
-fill the ExpType and find that the TcLevels don't work out, we
-fill the ExpType with a tau-tv at the low TcLevel, hopefully to
-be worked out later by some means. This is triggered in
-test gadt/gadt-escape1.
+fill the ExpType and find that the TcLevels don't work out, we fill
+the ExpType with a tau-tv at the low TcLevel, hopefully to be worked
+out later by some means -- see fillInferResult, and Note [fillInferResult]
+This behaviour triggered in test gadt/gadt-escape1.
-}
-- actual data definition is in GHC.Tc.Utils.TcType
@@ -453,6 +445,12 @@ readExpType_maybe :: ExpType -> TcM (Maybe TcType)
readExpType_maybe (Check ty) = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
+-- | Same as readExpType, but for Scaled ExpTypes
+readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
+readScaledExpType (Scaled m exp_ty)
+ = do { ty <- readExpType exp_ty
+ ; return (Scaled m ty) }
+
-- | Extract a type out of an ExpType. Otherwise, panics.
readExpType :: ExpType -> TcM TcType
readExpType exp_ty
@@ -472,12 +470,10 @@ checkingExpType :: String -> ExpType -> TcType
checkingExpType _ (Check ty) = ty
checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
-tauifyExpType :: ExpType -> TcM ExpType
--- ^ Turn a (Infer hole) type into a (Check alpha),
--- where alpha is a fresh unification variable
-tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
-tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
- ; return (Check ty) }
+scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
+scaledExpTypeToType (Scaled m exp_ty)
+ = do { ty <- expTypeToType exp_ty
+ ; return (Scaled m ty) }
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
@@ -488,209 +484,284 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res
inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
, ir_ref = ref })
- = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
- ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
- -- See Note [TcLevel of ExpType]
- ; writeMutVar ref (Just tau)
+ = do { mb_inferred_ty <- readTcRef ref
+ ; tau <- case mb_inferred_ty of
+ Just ty -> do { ensureMonoType ty
+ -- See Note [inferResultToType]
+ ; return ty }
+ Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
+ ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
+ -- See Note [TcLevel of ExpType]
+ ; writeMutVar ref (Just tau)
+ ; return tau }
; traceTc "Forcing ExpType to be monomorphic:"
(ppr u <+> text ":=" <+> ppr tau)
; return tau }
+{- Note [inferResultToType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+expTypeToType and inferResultType convert an InferResult to a monotype.
+It must be a monotype because if the InferResult isn't already filled in,
+we fill it in with a unification variable (hence monotype). So to preserve
+order-independence we check for mono-type-ness even if it *is* filled in
+already.
+
+See also Note [TcLevel of ExpType] above, and
+Note [fillInferResult].
+-}
+
+-- | Infer a type using a fresh ExpType
+-- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
+tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
+tcInfer tc_check
+ = do { res_ty <- newInferExpType
+ ; result <- tc_check res_ty
+ ; res_ty <- readExpType res_ty
+ ; return (result, res_ty) }
+
+fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
+-- If co = fillInferResult t1 t2
+-- => co :: t1 ~ t2
+-- See Note [fillInferResult]
+fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+ , ir_ref = ref })
+ = do { mb_exp_res_ty <- readTcRef ref
+ ; case mb_exp_res_ty of
+ Just exp_res_ty
+ -> do { traceTc "Joining inferred ExpType" $
+ ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
+ ; cur_lvl <- getTcLevel
+ ; unless (cur_lvl `sameDepthAs` res_lvl) $
+ ensureMonoType act_res_ty
+ ; unifyType Nothing act_res_ty exp_res_ty }
+ Nothing
+ -> do { traceTc "Filling inferred ExpType" $
+ ppr u <+> text ":=" <+> ppr act_res_ty
+ ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty
+ ; writeTcRef ref (Just act_res_ty)
+ ; return prom_co }
+ }
+
+
+{- Note [fillInferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When inferring, we use fillInferResult to "fill in" the hole in InferResult
+ data InferResult = IR { ir_uniq :: Unique
+ , ir_lvl :: TcLevel
+ , ir_ref :: IORef (Maybe TcType) }
+
+There are two things to worry about:
+
+1. What if it is under a GADT or existential pattern match?
+ - GADTs: a unification variable (and Infer's hole is similar) is untouchable
+ - Existentials: be careful about skolem-escape
+
+2. What if it is filled in more than once? E.g. multiple branches of a case
+ case e of
+ T1 -> e1
+ T2 -> e2
+
+Our typing rules are:
+
+* The RHS of a existential or GADT alternative must always be a
+ monotype, regardless of the number of alternatives.
+
+* Multiple non-existential/GADT branches can have (the same)
+ higher rank type (#18412). E.g. this is OK:
+ case e of
+ True -> hr
+ False -> hr
+ where hr:: (forall a. a->a) -> Int
+ c.f. Section 7.1 of "Practical type inference for arbitrary-rank types"
+ We use choice (2) in that Section.
+ (GHC 8.10 and earlier used choice (1).)
+
+ But note that
+ case e of
+ True -> hr
+ False -> \x -> hr x
+ will fail, because we still /infer/ both branches, so the \x will get
+ a (monotype) unification variable, which will fail to unify with
+ (forall a. a->a)
+
+For (1) we can detect the GADT/existential situation by seeing that
+the current TcLevel is greater than that stored in ir_lvl of the Infer
+ExpType. We bump the level whenever we go past a GADT/existential match.
+
+Then, before filling the hole use promoteTcType to promote the type
+to the outer ir_lvl. promoteTcType does this
+ - create a fresh unification variable alpha at level ir_lvl
+ - emits an equality alpha[ir_lvl] ~ ty
+ - fills the hole with alpha
+That forces the type to be a monotype (since unification variables can
+only unify with monotypes); and catches skolem-escapes because the
+alpha is untouchable until the equality floats out.
+
+For (2), we simply look to see if the hole is filled already.
+ - if not, we promote (as above) and fill the hole
+ - if it is filled, we simply unify with the type that is
+ already there
+
+There is one wrinkle. Suppose we have
+ case e of
+ T1 -> e1 :: (forall a. a->a) -> Int
+ G2 -> e2
+where T1 is not GADT or existential, but G2 is a GADT. Then supppose the
+T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
+But now the G2 alternative must not *just* unify with that else we'd risk
+allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first
+we'd have filled the hole with a unification variable, which enforces a
+monotype.
+
+So if we check G2 second, we still want to emit a constraint that restricts
+the RHS to be a monotype. This is done by ensureMonoType, and it works
+by simply generating a constraint (alpha ~ ty), where alpha is a fresh
+unification variable. We discard the evidence.
+
+-}
{- *********************************************************************
* *
- SkolemTvs (immutable)
+ Promoting types
* *
********************************************************************* -}
-tc_inst_internal :: ([VarBndr TyVar flag] -> TcM (TCvSubst, [VarBndr TcTyVar flag]))
- -- ^ How to instantiate the type variables
- -> [VarBndr TyVar flag] -- ^ Type variable to instantiate
- -> Type -- ^ rho
- -> TcM ([(Name, VarBndr TcTyVar flag)], TcThetaType, TcType) -- ^ Result
- -- (type vars, preds (incl equalities), rho)
-tc_inst_internal _inst_tyvars [] rho =
- let -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- (theta, tau) = tcSplitPhiTy rho
- in
- return ([], theta, tau)
-tc_inst_internal inst_tyvars tyvars rho =
- do { (subst, tyvars') <- inst_tyvars tyvars
- ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
- tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars'
- ; return (tv_prs, theta, tau) }
-
-tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
- -- ^ How to instantiate the type variables
- -> Id -- ^ Type to instantiate
- -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
- -- (type vars, preds (incl equalities), rho)
-tcInstType inst_tyvars id =
- do { let (tyvars, rho) = splitForAllTys (idType id)
- tyvars' = mkTyVarBinders () tyvars
- ; (tv_prs, preds, rho) <- tc_inst_internal inst_tyvar_bndrs tyvars' rho
- ; let tv_prs' = map (\(name, bndr) -> (name, binderVar bndr)) tv_prs
- ; return (tv_prs', preds, rho) }
- where
- inst_tyvar_bndrs :: [VarBndr TyVar ()] -> TcM (TCvSubst, [VarBndr TcTyVar ()])
- inst_tyvar_bndrs bndrs = do { (subst, tvs) <- inst_tyvars $ binderVars bndrs
- ; let tvbnds = map (\tv -> Bndr tv ()) tvs
- ; return (subst, tvbnds) }
-
-tcInstTypeBndrs :: ([VarBndr TyVar Specificity] -> TcM (TCvSubst, [VarBndr TcTyVar Specificity]))
- -- ^ How to instantiate the type variables
- -> Id -- ^ Type to instantiate
- -> TcM ([(Name, VarBndr TcTyVar Specificity)], TcThetaType, TcType) -- ^ Result
- -- (type vars, preds (incl equalities), rho)
-tcInstTypeBndrs inst_tyvars id =
- let (tyvars, rho) = splitForAllTysInvis (idType id)
- in tc_inst_internal inst_tyvars tyvars rho
-
-tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type signature with skolem constants.
--- We could give them fresh names, but no need to do so
-tcSkolDFunType dfun
- = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
- ; return (map snd tv_prs, theta, tau) }
-
-tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
--- Make skolem constants, but do *not* give them new names, as above
--- Moreover, make them "super skolems"; see comments with superSkolemTv
--- see Note [Kind substitution when instantiating]
--- Precondition: tyvars should be ordered by scoping
-tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
-
-tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
-tcSuperSkolTyVar subst tv
- = (extendTvSubstWithClone subst tv new_tv, new_tv)
- where
- kind = substTyUnchecked subst (tyVarKind tv)
- new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
-
--- | Given a list of @['TyVar']@, skolemize the type variables,
--- returning a substitution mapping the original tyvars to the
--- skolems, and the list of newly bound skolems.
-tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
-
-tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
-
-tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
-
-tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
--- See Note [Skolemising type variables]
-tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
-
-tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar]
- -> TcM (TCvSubst, [TcTyVar])
--- Skolemise one level deeper, hence pushTcLevel
--- See Note [Skolemising type variables]
-tcInstSkolTyVarsPushLevel overlappable subst tvs
- = do { tc_lvl <- getTcLevel
- ; let pushed_lvl = pushTcLevel tc_lvl
- ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
-
-tcInstSkolTyVarsAt :: TcLevel -> Bool
- -> TCvSubst -> [TyVar]
- -> TcM (TCvSubst, [TcTyVar])
-tcInstSkolTyVarsAt lvl overlappable subst tvs
- = freshenTyCoVarsX new_skol_tv subst tvs
+ensureMonoType :: TcType -> TcM ()
+-- Assuming that the argument type is of kind (TYPE r),
+-- ensure that it is a /monotype/
+-- If it is not a monotype we can see right away (since unification
+-- varibles and type-function applications stand for monotypes), but
+-- we emit a Wanted equality just to delay the error message until later
+ensureMonoType res_ty
+ | isTauTy res_ty -- isTauTy doesn't need zonking or anything
+ = return ()
+ | otherwise
+ = do { mono_ty <- newOpenFlexiTyVarTy
+ ; let eq_orig = TypeEqOrigin { uo_actual = res_ty
+ , uo_expected = mono_ty
+ , uo_thing = Nothing
+ , uo_visible = False }
+
+ ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
+ ; return () }
+
+promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
+-- See Note [Promoting a type]
+-- See also Note [fillInferResult]
+-- promoteTcType level ty = (co, ty')
+-- * Returns ty' whose max level is just 'level'
+-- and whose kind is ~# to the kind of 'ty'
+-- and whose kind has form TYPE rr
+-- * and co :: ty ~ ty'
+-- * and emits constraints to justify the coercion
+promoteTcType dest_lvl ty
+ = do { cur_lvl <- getTcLevel
+ ; if (cur_lvl `sameDepthAs` dest_lvl)
+ then return (mkTcNomReflCo ty, ty)
+ else promote_it }
where
- details = SkolemTv lvl overlappable
- new_skol_tv name kind = mkTcTyVar name kind details
-
-------------------
-freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
--- ^ Give fresh uniques to a bunch of TyVars, but they stay
--- as TyVars, rather than becoming TcTyVars
--- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
-freshenTyVarBndrs = freshenTyCoVars mkTyVar
-
-freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
--- ^ Give fresh uniques to a bunch of CoVars
--- Used in "GHC.Tc.Instance.Family.newFamInst"
-freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
-
-------------------
-freshenTyCoVars :: (Name -> Kind -> TyCoVar)
- -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
-
-freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
- -> TCvSubst -> [TyCoVar]
- -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
-
-freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
- -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
--- This a complete freshening operation:
--- the skolems have a fresh unique, and a location from the monad
--- See Note [Skolemising type variables]
-freshenTyCoVarX mk_tcv subst tycovar
- = do { loc <- getSrcSpanM
- ; uniq <- newUnique
- ; let old_name = tyVarName tycovar
- new_name = mkInternalName uniq (getOccName old_name) loc
- new_kind = substTyUnchecked subst (tyVarKind tycovar)
- new_tcv = mk_tcv new_name new_kind
- subst1 = extendTCvSubstWithClone subst tycovar new_tcv
- ; return (subst1, new_tcv) }
-
-{- Note [Skolemising type variables]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The tcInstSkolTyVars family of functions instantiate a list of TyVars
-to fresh skolem TcTyVars. Important notes:
-
-a) Level allocation. We generally skolemise /before/ calling
- pushLevelAndCaptureConstraints. So we want their level to the level
- of the soon-to-be-created implication, which has a level ONE HIGHER
- than the current level. Hence the pushTcLevel. It feels like a
- slight hack.
-
-b) The [TyVar] should be ordered (kind vars first)
- See Note [Kind substitution when instantiating]
-
-c) It's a complete freshening operation: the skolems have a fresh
- unique, and a location from the monad
-
-d) The resulting skolems are
- non-overlappable for tcInstSkolTyVars,
- but overlappable for tcInstSuperSkolTyVars
- See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
- of where this matters.
-
-Note [Kind substitution when instantiating]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we instantiate a bunch of kind and type variables, first we
-expect them to be topologically sorted.
-Then we have to instantiate the kind variables, build a substitution
-from old variables to the new variables, then instantiate the type
-variables substituting the original kind.
+ promote_it :: TcM (TcCoercion, TcType)
+ promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
+ -- where alpha and rr are fresh and from level dest_lvl
+ = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
+ ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
+ ; let eq_orig = TypeEqOrigin { uo_actual = ty
+ , uo_expected = prom_ty
+ , uo_thing = Nothing
+ , uo_visible = False }
+
+ ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
+ ; return (co, prom_ty) }
+{-
+ dont_promote_it :: TcM (TcCoercion, TcType)
+ dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
+ = do { res_kind <- newOpenTypeKind
+ ; ki_co <- unifyKind Nothing (tcTypeKind ty) res_kind
+ ; let co = mkTcGReflRightCo Nominal ty ki_co
+ ; return (co, ty `mkCastTy` ki_co) }
+-}
-Exemple: If we want to instantiate
- [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
-we want
- [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
-instead of the buggous
- [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
+{- Note [Promoting a type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#12427)
+
+ data T where
+ MkT :: (Int -> Int) -> a -> T
+
+ h y = case y of MkT v w -> v
+
+We'll infer the RHS type with an expected type ExpType of
+ (IR { ir_lvl = l, ir_ref = ref, ... )
+where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
+match will increase the level, so we'll end up in tcSubType, trying to
+unify the type of v,
+ v :: Int -> Int
+with the expected type. But this attempt takes place at level (l+1),
+rightly so, since v's type could have mentioned existential variables,
+(like w's does) and we want to catch that.
+
+So we
+ - create a new meta-var alpha[l+1]
+ - fill in the InferRes ref cell 'ref' with alpha
+ - emit an equality constraint, thus
+ [W] alpha[l+1] ~ (Int -> Int)
+
+That constraint will float outwards, as it should, unless v's
+type mentions a skolem-captured variable.
+
+This approach fails if v has a higher rank type; see
+Note [Promotion and higher rank types]
+
+
+Note [Promotion and higher rank types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
+then we'd emit an equality
+ [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
+which will sadly fail because we can't unify a unification variable
+with a polytype. But there is nothing really wrong with the program
+here.
+
+We could just about solve this by "promote the type" of v, to expose
+its polymorphic "shape" while still leaving constraints that will
+prevent existential escape. But we must be careful! Exposing
+the "shape" of the type is precisely what we must NOT do under
+a GADT pattern match! So in this case we might promote the type
+to
+ (forall a. a->a) -> alpha[l+1]
+and emit the constraint
+ [W] alpha[l+1] ~ Int
+Now the promoted type can fill the ref cell, while the emitted
+equality can float or not, according to the usual rules.
+
+But that's not quite right! We are exposing the arrow! We could
+deal with that too:
+ (forall a. mu[l+1] a a) -> alpha[l+1]
+with constraints
+ [W] alpha[l+1] ~ Int
+ [W] mu[l+1] ~ (->)
+Here we abstract over the '->' inside the forall, in case that
+is subject to an equality constraint from a GADT match.
+
+Note that we kept the outer (->) because that's part of
+the polymorphic "shape". And because of impredicativity,
+GADT matches can't give equalities that affect polymorphic
+shape.
+
+This reasoning just seems too complicated, so I decided not
+to do it. These higher-rank notes are just here to record
+the thinking.
+-}
-************************************************************************
+{- *********************************************************************
* *
MetaTvs (meta type variables; mutable)
* *
-************************************************************************
--}
+********************************************************************* -}
-{-
-Note [TyVarTv]
-~~~~~~~~~~~~
+{- Note [TyVarTv]
+~~~~~~~~~~~~~~~~~
A TyVarTv can unify with type *variables* only, including other TyVarTvs and
skolems. Sometimes, they can unify with type variables that the user would
@@ -1031,18 +1102,11 @@ newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
-newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
-
-newMetaTyVarTyVars :: [VarBndr TyVar Specificity]
- -> TcM (TCvSubst, [VarBndr TcTyVar Specificity])
-newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
+newMetaTyVarX = new_meta_tv_x TauTv
-newMetaTyVarTyVarX :: TCvSubst -> (VarBndr TyVar Specificity)
- -> TcM (TCvSubst, VarBndr TcTyVar Specificity)
+newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a TyVarTv
-newMetaTyVarTyVarX subst (Bndr tv spec) =
- do { (subst', tv') <- new_meta_tv_x TyVarTv subst tv
- ; return (subst', (Bndr tv' spec)) }
+newMetaTyVarTyVarX = new_meta_tv_x TyVarTv
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -57,7 +57,7 @@ module GHC.Tc.Utils.TcType (
-- These are important because they do not look through newtypes
getTyVar,
tcSplitForAllTy_maybe,
- tcSplitForAllTys, tcSplitSomeForAllTys,
+ tcSplitForAllTys,
tcSplitForAllTysReq, tcSplitForAllTysInvis,
tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs,
tcSplitPhiTy, tcSplitPredFunTy_maybe,
@@ -1221,14 +1221,6 @@ tcSplitForAllTys ty
= ASSERT( all isTyVar (fst sty) ) sty
where sty = splitForAllTys ty
--- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@
--- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
--- @argf_pred@ is a predicate over visibilities provided as an argument to this
--- function. All split tyvars are annotated with their @argf at .
-tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type)
-tcSplitSomeForAllTys argf_pred ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty
- where sty = splitSomeForAllTys argf_pred ty
-
-- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type
-- variable binders. All split tyvars are annotated with '()'.
tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -61,7 +61,6 @@ import GHC.Types.Name( isSystemName )
import GHC.Tc.Utils.Instantiate
import GHC.Core.TyCon
import GHC.Builtin.Types
-import GHC.Builtin.Types.Prim( tYPE )
import GHC.Types.Var as Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
@@ -571,10 +570,51 @@ tcSubTypeNC :: CtOrigin -- Used when instantiating
-> TcM HsWrapper
tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
= case res_ty of
- Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res
Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
ty_actual ty_expected
+ Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
+ -- See Note [Instantiation of InferResult]
+ ; co <- fillInferResult rho inf_res
+ ; return (mkWpCastN co <.> wrap) }
+
+{- Note [Instantiation of InferResult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We now always instantiate before filling in InferResult, so that
+the result is a TcRhoType: see #17173 for discussion.
+
+For example:
+
+1. Consider
+ f x = (*)
+ We want to instantiate the type of (*) before returning, else we
+ will infer the type
+ f :: forall {a}. a -> forall b. Num b => b -> b -> b
+ This is surely confusing for users.
+
+ And worse, the monomorphism restriction won't work properly. The MR is
+ dealt with in simplifyInfer, and simplifyInfer has no way of
+ instantiating. This could perhaps be worked around, but it may be
+ hard to know even when instantiation should happen.
+
+2. Another reason. Consider
+ f :: (?x :: Int) => a -> a
+ g y = let ?x = 3::Int in f
+ Here want to instantiate f's type so that the ?x::Int constraint
+ gets discharged by the enclosing implicit-parameter binding.
+
+3. Suppose one defines plus = (+). If we instantiate lazily, we will
+ infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
+ restriction compels us to infer
+ plus :: Integer -> Integer -> Integer
+ (or similar monotype). Indeed, the only way to know whether to apply
+ the monomorphism restriction at all is to instantiate
+
+There is one place where we don't want to instantiate eagerly,
+namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
+command. See Note [Implementing :type] in GHC.Tc.Module.
+-}
+
---------------
tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- External entry point, but no ExpTypes on either side
@@ -768,213 +808,6 @@ tcEqMult origin w_actual w_expected = do
; coercion <- uType TypeLevel origin w_actual w_expected
; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
-{- **********************************************************************
-%* *
- ExpType functions: tcInfer, instantiateAndFillInferResult
-%* *
-%********************************************************************* -}
-
--- | Infer a type using a fresh ExpType
--- See also Note [ExpType] in "GHC.Tc.Utils.TcMType"
-tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType)
-tcInfer tc_check
- = do { res_ty <- newInferExpType
- ; result <- tc_check res_ty
- ; res_ty <- readExpType res_ty
- ; return (result, res_ty) }
-
-instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper
--- If wrap = instantiateAndFillInferResult t1 t2
--- => wrap :: t1 ~> t2
--- See Note [Instantiation of InferResult]
-instantiateAndFillInferResult orig ty inf_res
- = do { (wrap, rho) <- topInstantiate orig ty
- ; co <- fillInferResult rho inf_res
- ; return (mkWpCastN co <.> wrap) }
-
-fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fillInferResult t1 t2
--- => wrap :: t1 ~> t2
-fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
- , ir_ref = ref })
- = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
-
- ; traceTc "Filling ExpType" $
- ppr u <+> text ":=" <+> ppr ty_to_fill_with
-
- ; when debugIsOn (check_hole ty_to_fill_with)
-
- ; writeTcRef ref (Just ty_to_fill_with)
-
- ; return ty_co }
- where
- check_hole ty -- Debug check only
- = do { let ty_lvl = tcTypeLevel ty
- ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
- ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
- ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
- ; cts <- readTcRef ref
- ; case cts of
- Just already_there -> pprPanic "writeExpType"
- (vcat [ ppr u
- , ppr ty
- , ppr already_there ])
- Nothing -> return () }
-
-{- Note [Instantiation of InferResult]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We now always instantiate before filling in InferResult, so that
-the result is a TcRhoType: see #17173 for discussion.
-
-For example:
-
-1. Consider
- f x = (*)
- We want to instantiate the type of (*) before returning, else we
- will infer the type
- f :: forall {a}. a -> forall b. Num b => b -> b -> b
- This is surely confusing for users.
-
- And worse, the monomorphism restriction won't work properly. The MR is
- dealt with in simplifyInfer, and simplifyInfer has no way of
- instantiating. This could perhaps be worked around, but it may be
- hard to know even when instantiation should happen.
-
-2. Another reason. Consider
- f :: (?x :: Int) => a -> a
- g y = let ?x = 3::Int in f
- Here want to instantiate f's type so that the ?x::Int constraint
- gets discharged by the enclosing implicit-parameter binding.
-
-3. Suppose one defines plus = (+). If we instantiate lazily, we will
- infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism
- restriction compels us to infer
- plus :: Integer -> Integer -> Integer
- (or similar monotype). Indeed, the only way to know whether to apply
- the monomorphism restriction at all is to instantiate
-
-There is one place where we don't want to instantiate eagerly,
-namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
-command. See Note [Implementing :type] in GHC.Tc.Module.
-
--}
-
-{- *********************************************************************
-* *
- Promoting types
-* *
-********************************************************************* -}
-
-promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
--- See Note [Promoting a type]
--- promoteTcType level ty = (co, ty')
--- * Returns ty' whose max level is just 'level'
--- and whose kind is ~# to the kind of 'ty'
--- and whose kind has form TYPE rr
--- * and co :: ty ~ ty'
--- * and emits constraints to justify the coercion
-promoteTcType dest_lvl ty
- = do { cur_lvl <- getTcLevel
- ; if (cur_lvl `sameDepthAs` dest_lvl)
- then dont_promote_it
- else promote_it }
- where
- promote_it :: TcM (TcCoercion, TcType)
- promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
- -- where alpha and rr are fresh and from level dest_lvl
- = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
- ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
- ; let eq_orig = TypeEqOrigin { uo_actual = ty
- , uo_expected = prom_ty
- , uo_thing = Nothing
- , uo_visible = False }
-
- ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
- ; return (co, prom_ty) }
-
- dont_promote_it :: TcM (TcCoercion, TcType)
- dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
- = do { res_kind <- newOpenTypeKind
- ; let ty_kind = tcTypeKind ty
- kind_orig = TypeEqOrigin { uo_actual = ty_kind
- , uo_expected = res_kind
- , uo_thing = Nothing
- , uo_visible = False }
- ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
- ; let co = mkTcGReflRightCo Nominal ty ki_co
- ; return (co, ty `mkCastTy` ki_co) }
-
-{- Note [Promoting a type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#12427)
-
- data T where
- MkT :: (Int -> Int) -> a -> T
-
- h y = case y of MkT v w -> v
-
-We'll infer the RHS type with an expected type ExpType of
- (IR { ir_lvl = l, ir_ref = ref, ... )
-where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
-match will increase the level, so we'll end up in tcSubType, trying to
-unify the type of v,
- v :: Int -> Int
-with the expected type. But this attempt takes place at level (l+1),
-rightly so, since v's type could have mentioned existential variables,
-(like w's does) and we want to catch that.
-
-So we
- - create a new meta-var alpha[l+1]
- - fill in the InferRes ref cell 'ref' with alpha
- - emit an equality constraint, thus
- [W] alpha[l+1] ~ (Int -> Int)
-
-That constraint will float outwards, as it should, unless v's
-type mentions a skolem-captured variable.
-
-This approach fails if v has a higher rank type; see
-Note [Promotion and higher rank types]
-
-
-Note [Promotion and higher rank types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
-then we'd emit an equality
- [W] alpha[l+1] ~ ((forall a. a->a) -> Int)
-which will sadly fail because we can't unify a unification variable
-with a polytype. But there is nothing really wrong with the program
-here.
-
-We could just about solve this by "promote the type" of v, to expose
-its polymorphic "shape" while still leaving constraints that will
-prevent existential escape. But we must be careful! Exposing
-the "shape" of the type is precisely what we must NOT do under
-a GADT pattern match! So in this case we might promote the type
-to
- (forall a. a->a) -> alpha[l+1]
-and emit the constraint
- [W] alpha[l+1] ~ Int
-Now the promoted type can fill the ref cell, while the emitted
-equality can float or not, according to the usual rules.
-
-But that's not quite right! We are exposing the arrow! We could
-deal with that too:
- (forall a. mu[l+1] a a) -> alpha[l+1]
-with constraints
- [W] alpha[l+1] ~ Int
- [W] mu[l+1] ~ (->)
-Here we abstract over the '->' inside the forall, in case that
-is subject to an equality constraint from a GADT match.
-
-Note that we kept the outer (->) because that's part of
-the polymorphic "shape". And because of impredicativity,
-GADT matches can't give equalities that affect polymorphic
-shape.
-
-This reasoning just seems too complicated, so I decided not
-to do it. These higher-rank notes are just here to record
-the thinking.
--}
{- *********************************************************************
* *
=====================================
testsuite/tests/simplCore/should_compile/T17901.stdout
=====================================
@@ -1,14 +1,14 @@
- (wombat1 [Occ=Once*!] :: T -> p)
+ (wombat1 [Occ=Once*!] :: T -> t)
A -> wombat1 T17901.A;
B -> wombat1 T17901.B;
C -> wombat1 T17901.C
- = \ (@p) (wombat1 :: T -> p) (x :: T) ->
+ = \ (@t) (wombat1 :: T -> t) (x :: T) ->
case x of wild { __DEFAULT -> wombat1 wild }
- Tmpl= \ (@p) (wombat2 [Occ=Once!] :: S -> p) (x [Occ=Once] :: S) ->
+ Tmpl= \ (@t) (wombat2 [Occ=Once!] :: S -> t) (x [Occ=Once] :: S) ->
case x of wild [Occ=Once] { __DEFAULT -> wombat2 wild }}]
- = \ (@p) (wombat2 :: S -> p) (x :: S) ->
+ = \ (@t) (wombat2 :: S -> t) (x :: S) ->
case x of wild { __DEFAULT -> wombat2 wild }
- Tmpl= \ (@p) (wombat3 [Occ=Once!] :: W -> p) (x [Occ=Once] :: W) ->
+ Tmpl= \ (@t) (wombat3 [Occ=Once!] :: W -> t) (x [Occ=Once] :: W) ->
case x of wild [Occ=Once] { __DEFAULT -> wombat3 wild }}]
- = \ (@p) (wombat3 :: W -> p) (x :: W) ->
+ = \ (@t) (wombat3 :: W -> t) (x :: W) ->
case x of wild { __DEFAULT -> wombat3 wild }
=====================================
testsuite/tests/typecheck/should_compile/T18412.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T18412 where
+
+hr :: (forall a. a -> a) -> ()
+hr _ = ()
+
+foo x = case x of () -> hr
+
+-- This did not use to be allowed, because the
+-- multiple branches have (the same) polytypes
+-- Enhancement July 2020
+bar x = case x of True -> hr
+ False -> hr
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -716,3 +716,4 @@ test('T17775-viewpats-a', normal, compile, [''])
test('T17775-viewpats-b', normal, compile_fail, [''])
test('T17775-viewpats-c', normal, compile_fail, [''])
test('T17775-viewpats-d', normal, compile_fail, [''])
+test('T18412', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T10619.stderr
=====================================
@@ -1,13 +1,11 @@
-T10619.hs:9:15: error:
- • Couldn't match type ‘p’ with ‘forall b. b -> b’
- Expected: p -> p
- Actual: (forall a. a -> a) -> forall b. b -> b
- ‘p’ is a rigid type variable bound by
- the inferred type of foo :: p1 -> p -> p
- at T10619.hs:(8,1)-(10,20)
- • In the expression:
- (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
+T10619.hs:10:14: error:
+ • Couldn't match type ‘p1’ with ‘forall a. a -> a’
+ Expected: (forall a. a -> a) -> forall b. b -> b
+ Actual: p1 -> p1
+ Cannot instantiate unification variable ‘p1’
+ with a type involving polytypes: forall a. a -> a
+ • In the expression: \ y -> y
In the expression:
if True then
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
@@ -19,15 +17,13 @@ T10619.hs:9:15: error:
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
else
\ y -> y
- • Relevant bindings include
- foo :: p1 -> p -> p (bound at T10619.hs:8:1)
T10619.hs:14:15: error:
• Couldn't match type ‘p’ with ‘forall a. a -> a’
Expected: p -> p
Actual: (forall a. a -> a) -> forall b. b -> b
‘p’ is a rigid type variable bound by
- the inferred type of bar :: p1 -> p -> p
+ the inferred type of bar :: p2 -> p -> p
at T10619.hs:(12,1)-(14,66)
• In the expression:
(\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
@@ -43,21 +39,16 @@ T10619.hs:14:15: error:
else
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
• Relevant bindings include
- bar :: p1 -> p -> p (bound at T10619.hs:12:1)
+ bar :: p2 -> p -> p (bound at T10619.hs:12:1)
-T10619.hs:16:13: error:
- • Couldn't match type ‘p’ with ‘forall b. b -> b’
- Expected: p -> p
- Actual: (forall a. a -> a) -> forall b. b -> b
- ‘p’ is a rigid type variable bound by
- the inferred type of baz :: Bool -> p -> p
- at T10619.hs:(16,1)-(17,19)
- • In the expression:
- (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
- In an equation for ‘baz’:
- baz True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
- • Relevant bindings include
- baz :: Bool -> p -> p (bound at T10619.hs:16:1)
+T10619.hs:17:13: error:
+ • Couldn't match type ‘p0’ with ‘forall a. a -> a’
+ Expected: (forall a. a -> a) -> forall b. b -> b
+ Actual: p0 -> p0
+ Cannot instantiate unification variable ‘p0’
+ with a type involving polytypes: forall a. a -> a
+ • In the expression: \ y -> y
+ In an equation for ‘baz’: baz False = \ y -> y
T10619.hs:20:14: error:
• Couldn't match type ‘p’ with ‘forall a. a -> a’
=====================================
testsuite/tests/typecheck/should_fail/VtaFail.stderr
=====================================
@@ -7,7 +7,7 @@ VtaFail.hs:7:16: error:
answer_nosig = pairup_nosig @Int @Bool 5 True
VtaFail.hs:14:17: error:
- • Cannot apply expression of type ‘p0 -> p0’
+ • Cannot apply expression of type ‘p1 -> p1’
to a visible type argument ‘Int’
• In the expression: (\ x -> x) @Int 12
In an equation for ‘answer_lambda’:
=====================================
testsuite/tests/typecheck/should_fail/tcfail002.stderr
=====================================
@@ -1,8 +1,8 @@
tcfail002.hs:4:7: error:
- • Couldn't match expected type ‘p’ with actual type ‘[p]’
+ • Couldn't match expected type ‘a’ with actual type ‘[a]’
• In the expression: z
In an equation for ‘c’: c z = z
• Relevant bindings include
- z :: [p] (bound at tcfail002.hs:4:3)
- c :: [p] -> p (bound at tcfail002.hs:3:1)
+ z :: [a] (bound at tcfail002.hs:4:3)
+ c :: [a] -> a (bound at tcfail002.hs:3:1)
=====================================
testsuite/tests/typecheck/should_fail/tcfail104.stderr
=====================================
@@ -1,19 +1,22 @@
-tcfail104.hs:14:12: error:
+tcfail104.hs:16:12: error:
+ • Couldn't match type: Char -> Char
+ with: forall a. a -> a
+ Expected: (forall a. a -> a) -> Char -> Char
+ Actual: (Char -> Char) -> Char -> Char
+ • In the expression: \ x -> x
+ In the expression:
+ if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+ In the expression:
+ (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
+
+tcfail104.hs:22:12: error:
• Couldn't match type: forall a. a -> a
with: Char -> Char
Expected: (Char -> Char) -> Char -> Char
Actual: (forall a. a -> a) -> Char -> Char
• In the expression: \ (x :: forall a. a -> a) -> x
In the expression:
- if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+ if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)
In the expression:
- (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
-
-tcfail104.hs:22:15: error:
- • Couldn't match expected type: Char -> Char
- with actual type: forall a. a -> a
- • When checking that the pattern signature: forall a. a -> a
- fits the type of its context: Char -> Char
- In the pattern: x :: forall a. a -> a
- In the expression: \ (x :: forall a. a -> a) -> x
+ (if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)) id 'c'
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a60e30e08a0c59687e39f0eee9be1e539ee6f0d1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a60e30e08a0c59687e39f0eee9be1e539ee6f0d1
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/20200714/ad4ee7ad/attachment-0001.html>
More information about the ghc-commits
mailing list