diff options
94 files changed, 3412 insertions, 2119 deletions
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index 251fae2c48..11a102f91b 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -40,6 +40,7 @@ import GHC.Hs.Binds -- others: import GHC.Tc.Types.Evidence import GHC.Core +import GHC.Types.Id( Id ) import GHC.Types.Name import GHC.Types.Name.Set import GHC.Types.Basic @@ -251,8 +252,8 @@ data HsExpr p -- Turned from HsVar to HsUnboundVar by the -- renamer, when it finds an out-of-scope -- variable or hole. - -- Turned into HsVar by type checker, to support - -- deferred type errors. + -- The (XUnboundVar p) field becomes Id + -- after typechecking | HsConLikeOut (XConLikeOut p) ConLike -- ^ After typechecker only; must be different @@ -260,7 +261,9 @@ data HsExpr p | HsRecFld (XRecFld p) (AmbiguousFieldOcc p) -- ^ Variable pointing to record selector - -- Not in use after typechecking + -- The parser produces HsVars + -- The renamer renames record-field selectors to HsRecFld + -- The typechecker preserves HsRecFld | HsOverLabel (XOverLabel p) (Maybe (IdP p)) FastString @@ -592,7 +595,6 @@ deriving instance (Data (hs_syn GhcTc), Typeable hs_syn) => Data (HsWrap hs_syn) -- --------------------------------------------------------------------- type instance XVar (GhcPass _) = NoExtField -type instance XUnboundVar (GhcPass _) = NoExtField type instance XConLikeOut (GhcPass _) = NoExtField type instance XRecFld (GhcPass _) = NoExtField type instance XOverLabel (GhcPass _) = NoExtField @@ -603,6 +605,10 @@ type instance XLam (GhcPass _) = NoExtField type instance XLamCase (GhcPass _) = NoExtField type instance XApp (GhcPass _) = NoExtField +type instance XUnboundVar GhcPs = NoExtField +type instance XUnboundVar GhcRn = NoExtField +type instance XUnboundVar GhcTc = Id + type instance XAppTypeE GhcPs = NoExtField type instance XAppTypeE GhcRn = NoExtField type instance XAppTypeE GhcTc = Type @@ -1049,14 +1055,15 @@ ppr_lexpr e = ppr_expr (unLoc e) ppr_expr :: forall p. (OutputableBndrId p) => HsExpr (GhcPass p) -> SDoc -ppr_expr (HsVar _ (L _ v)) = pprPrefixOcc v -ppr_expr (HsUnboundVar _ uv)= pprPrefixOcc uv -ppr_expr (HsConLikeOut _ c) = pprPrefixOcc c -ppr_expr (HsIPVar _ v) = ppr v -ppr_expr (HsOverLabel _ _ l)= char '#' <> ppr l -ppr_expr (HsLit _ lit) = ppr lit -ppr_expr (HsOverLit _ lit) = ppr lit -ppr_expr (HsPar _ e) = parens (ppr_lexpr e) +ppr_expr (HsVar _ (L _ v)) = pprPrefixOcc v +ppr_expr (HsUnboundVar _ uv) = pprPrefixOcc uv +ppr_expr (HsConLikeOut _ c) = pprPrefixOcc c +ppr_expr (HsRecFld _ f) = pprPrefixOcc f +ppr_expr (HsIPVar _ v) = ppr v +ppr_expr (HsOverLabel _ _ l) = char '#' <> ppr l +ppr_expr (HsLit _ lit) = ppr lit +ppr_expr (HsOverLit _ lit) = ppr lit +ppr_expr (HsPar _ e) = parens (ppr_lexpr e) ppr_expr (HsPragE _ prag e) = sep [ppr prag, ppr_lexpr e] @@ -1212,7 +1219,6 @@ ppr_expr (HsBinTick _ tickIdTrue tickIdFalse exp) text ">(", ppr exp, text ")"] -ppr_expr (HsRecFld _ f) = ppr f ppr_expr (XExpr x) = case ghcPass @p of #if __GLASGOW_HASKELL__ < 811 GhcPs -> ppr x @@ -1377,7 +1383,6 @@ isAtomicHsExpr (HsOverLit {}) = True isAtomicHsExpr (HsIPVar {}) = True isAtomicHsExpr (HsOverLabel {}) = True isAtomicHsExpr (HsUnboundVar {}) = True -isAtomicHsExpr (HsPar _ e) = isAtomicHsExpr (unLoc e) isAtomicHsExpr (HsRecFld{}) = True isAtomicHsExpr (XExpr x) | GhcTc <- ghcPass @p = case x of diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs index b1507f0adc..8ce29a72d3 100644 --- a/compiler/GHC/Hs/Pat.hs +++ b/compiler/GHC/Hs/Pat.hs @@ -478,7 +478,7 @@ data HsRecField' id arg = HsRecField { -- -- hsRecFieldLbl = Unambiguous "x" $sel:x:MkS :: AmbiguousFieldOcc Id -- --- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Expr. +-- See also Note [Disambiguating record fields] in GHC.Tc.Gen.Head. hsRecFields :: HsRecFields p arg -> [XCFieldOcc p] hsRecFields rbinds = map (unLoc . hsRecFieldSel . unLoc) (rec_flds rbinds) diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs index 65210d1044..c2da3857d4 100644 --- a/compiler/GHC/Hs/Type.hs +++ b/compiler/GHC/Hs/Type.hs @@ -348,7 +348,7 @@ data HsForAllTelescope pass { hsf_xvis :: XHsForAllVis pass , hsf_vis_bndrs :: [LHsTyVarBndr () pass] } - | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@), + | HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c. {...}@), -- where each binder has a 'Specificity'. { hsf_xinvis :: XHsForAllInvis pass , hsf_invis_bndrs :: [LHsTyVarBndr Specificity pass] @@ -1712,7 +1712,7 @@ mkFieldOcc rdr = FieldOcc noExtField rdr -- occurrences). -- -- See Note [HsRecField and HsRecUpdField] in "GHC.Hs.Pat" and --- Note [Disambiguating record fields] in "GHC.Tc.Gen.Expr". +-- Note [Disambiguating record fields] in "GHC.Tc.Gen.Head". -- See Note [Located RdrNames] in "GHC.Hs.Expr" data AmbiguousFieldOcc pass = Unambiguous (XUnambiguous pass) (Located RdrName) diff --git a/compiler/GHC/HsToCore/Coverage.hs b/compiler/GHC/HsToCore/Coverage.hs index 59c0bfb4ed..ae8c5a3b83 100644 --- a/compiler/GHC/HsToCore/Coverage.hs +++ b/compiler/GHC/HsToCore/Coverage.hs @@ -505,23 +505,25 @@ addBinTickLHsExpr boxLabel (L pos e0) -- in the addTickLHsExpr family of functions.) addTickHsExpr :: HsExpr GhcTc -> TM (HsExpr GhcTc) -addTickHsExpr e@(HsVar _ (L _ id)) = do freeVar id; return e -addTickHsExpr (HsUnboundVar {}) = panic "addTickHsExpr.HsUnboundVar" +addTickHsExpr e@(HsVar _ (L _ id)) = do freeVar id; return e +addTickHsExpr e@(HsUnboundVar id _) = do freeVar id; return e +addTickHsExpr e@(HsRecFld _ (Ambiguous id _)) = do freeVar id; return e +addTickHsExpr e@(HsRecFld _ (Unambiguous id _)) = do freeVar id; return e addTickHsExpr e@(HsConLikeOut _ con) | Just id <- conLikeWrapId_maybe con = do freeVar id; return e -addTickHsExpr e@(HsIPVar {}) = return e -addTickHsExpr e@(HsOverLit {}) = return e -addTickHsExpr e@(HsOverLabel{}) = return e -addTickHsExpr e@(HsLit {}) = return e -addTickHsExpr (HsLam x matchgroup) = liftM (HsLam x) - (addTickMatchGroup True matchgroup) -addTickHsExpr (HsLamCase x mgs) = liftM (HsLamCase x) - (addTickMatchGroup True mgs) -addTickHsExpr (HsApp x e1 e2) = liftM2 (HsApp x) (addTickLHsExprNever e1) - (addTickLHsExpr e2) -addTickHsExpr (HsAppType x e ty) = liftM3 HsAppType (return x) - (addTickLHsExprNever e) - (return ty) +addTickHsExpr e@(HsIPVar {}) = return e +addTickHsExpr e@(HsOverLit {}) = return e +addTickHsExpr e@(HsOverLabel{}) = return e +addTickHsExpr e@(HsLit {}) = return e +addTickHsExpr (HsLam x mg) = liftM (HsLam x) + (addTickMatchGroup True mg) +addTickHsExpr (HsLamCase x mgs) = liftM (HsLamCase x) + (addTickMatchGroup True mgs) +addTickHsExpr (HsApp x e1 e2) = liftM2 (HsApp x) (addTickLHsExprNever e1) + (addTickLHsExpr e2) +addTickHsExpr (HsAppType x e ty) = liftM3 HsAppType (return x) + (addTickLHsExprNever e) + (return ty) addTickHsExpr (OpApp fix e1 e2 e3) = liftM4 OpApp diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index be61777722..783e8b098b 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -261,10 +261,14 @@ dsLExprNoLP (L loc e) ; return e' } dsExpr :: HsExpr GhcTc -> DsM CoreExpr +dsExpr (HsVar _ (L _ id)) = dsHsVar id +dsExpr (HsRecFld _ (Unambiguous id _)) = dsHsVar id +dsExpr (HsRecFld _ (Ambiguous id _)) = dsHsVar id +dsExpr (HsUnboundVar id _) = dsHsVar id + dsExpr (HsPar _ e) = dsLExpr e dsExpr (ExprWithTySig _ e _) = dsLExpr e -dsExpr (HsVar _ (L _ var)) = dsHsVar var -dsExpr (HsUnboundVar {}) = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them + dsExpr (HsConLikeOut _ con) = dsConLike con dsExpr (HsIPVar {}) = panic "dsExpr: HsIPVar" dsExpr (HsOverLabel{}) = panic "dsExpr: HsOverLabel" @@ -806,7 +810,6 @@ dsExpr (HsBinTick _ ixT ixF e) = do -- HsSyn constructs that just shouldn't be here: dsExpr (HsBracket {}) = panic "dsExpr:HsBracket" dsExpr (HsDo {}) = panic "dsExpr:HsDo" -dsExpr (HsRecFld {}) = panic "dsExpr:HsRecFld" ds_prag_expr :: HsPragE GhcTc -> LHsExpr GhcTc -> DsM CoreExpr ds_prag_expr (HsPragSCC _ _ cc) expr = do diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs index b123450b60..ffc9c0a742 100644 --- a/compiler/GHC/Iface/Ext/Ast.hs +++ b/compiler/GHC/Iface/Ext/Ast.hs @@ -785,6 +785,7 @@ class ( IsPass p , Data (HsTupArg (GhcPass p)) , Data (IPBind (GhcPass p)) , ToHie (Context (Located (IdGhcP p))) + , ToHie (Context (Located (XUnboundVar (GhcPass p)))) , ToHie (RFContext (Located (AmbiguousFieldOcc (GhcPass p)))) , ToHie (RFContext (Located (FieldOcc (GhcPass p)))) , ToHie (TScoped (LHsWcType (GhcPass (NoGhcTcPass p)))) @@ -799,6 +800,9 @@ instance HiePass 'Renamed where instance HiePass 'Typechecked where hiePass = HieTc +instance ToHie (Context (Located NoExtField)) where + toHie _ = pure [] + instance HiePass p => ToHie (BindContext (Located (HsBind (GhcPass p)))) where toHie (BC context scope b@(L span bind)) = concatM $ getTypeNode b : case bind of @@ -1042,8 +1046,8 @@ instance HiePass p => ToHie (Located (HsExpr (GhcPass p))) where [ toHie $ C Use (L mspan var) -- Patch up var location since typechecker removes it ] - HsUnboundVar _ _ -> - [] + HsUnboundVar var _ -> + [ toHie $ C Use (L mspan var) ] HsConLikeOut _ con -> [ toHie $ C Use $ L mspan $ conLikeName con ] diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs index ecf31c01ea..9014c9f159 100644 --- a/compiler/GHC/Parser/PostProcess.hs +++ b/compiler/GHC/Parser/PostProcess.hs @@ -1634,7 +1634,7 @@ patSynErr item l e explanation = explanation ; return (L l hsHoleExpr) } -hsHoleExpr :: HsExpr (GhcPass id) +hsHoleExpr :: HsExpr GhcPs hsHoleExpr = HsUnboundVar noExtField (mkVarOcc "_") -- | See Note [Ambiguous syntactic categories] and Note [PatBuilder] diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs index f0cd54358f..72058a2512 100644 --- a/compiler/GHC/Rename/Pat.hs +++ b/compiler/GHC/Rename/Pat.hs @@ -749,7 +749,7 @@ rnHsRecUpdFields flds = do { let lbl = rdrNameAmbiguousFieldOcc f ; sel <- setSrcSpan loc $ -- Defer renaming of overloaded fields to the typechecker - -- See Note [Disambiguating record fields] in GHC.Tc.Gen.Expr + -- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head if overload_ok then do { mb <- lookupGlobalOccRn_overloaded overload_ok lbl diff --git a/compiler/GHC/Runtime/Eval.hs b/compiler/GHC/Runtime/Eval.hs index 0891da5808..aad557579b 100644 --- a/compiler/GHC/Runtime/Eval.hs +++ b/compiler/GHC/Runtime/Eval.hs @@ -81,7 +81,6 @@ import GHC.ByteCode.Types import GHC.Runtime.Linker as Linker import GHC.Driver.Session import GHC.Driver.Ppr -import GHC.LanguageExtensions import GHC.Types.Unique import GHC.Types.Unique.Supply import GHC.Utils.Monad @@ -1283,10 +1282,7 @@ obtainTermFromVal hsc_env _bound _force _ty _x = withInterp hsc_env $ \case obtainTermFromId :: HscEnv -> Int -> Bool -> Id -> IO Term obtainTermFromId hsc_env bound force id = do hv <- Linker.getHValue hsc_env (varName id) - cvObtainTerm (updEnv hsc_env) bound force (idType id) hv - where updEnv env = env {hsc_dflags = -- #14828 - xopt_set (hsc_dflags env) ImpredicativeTypes} - -- See Note [Setting ImpredicativeTypes for :print command] + cvObtainTerm hsc_env bound force (idType id) hv -- Uses RTTI to reconstruct the type of an Id, making it less polymorphic reconstructType :: HscEnv -> Int -> Id -> IO (Maybe Type) @@ -1296,39 +1292,3 @@ reconstructType hsc_env bound id = do mkRuntimeUnkTyVar :: Name -> Kind -> TyVar mkRuntimeUnkTyVar name kind = mkTcTyVar name kind RuntimeUnk - - -{- -Note [Setting ImpredicativeTypes for :print command] - -If ImpredicativeTypes is not enabled, then `:print <term>` will fail if the -type of <term> has nested `forall`s or `=>`s. -This is because the GHCi debugger's internals will attempt to unify a -metavariable with the type of <term> and then display the result, but if the -type has nested `forall`s or `=>`s, then unification will fail. -As a result, `:print` will bail out and the unhelpful result will be -`<term> = (_t1::t1)` (where `t1` is a metavariable). - -Beware: <term> can have nested `forall`s even if its definition doesn't use -RankNTypes! Here is an example from #14828: - - class Functor f where - fmap :: (a -> b) -> f a -> f b - -Somewhat surprisingly, `:print fmap` considers the type of fmap to have -nested foralls. This is because the GHCi debugger sees the type -`fmap :: forall f. Functor f => forall a b. (a -> b) -> f a -> f b`. -We could envision deeply instantiating this type to get the type -`forall f a b. Functor f => (a -> b) -> f a -> f b`, -but this trick wouldn't work for higher-rank types. - -Instead, we adopt a simpler fix: enable `ImpredicativeTypes` when using -`:print` and friends in the GHCi debugger. This allows metavariables -to unify with types that have nested (or higher-rank) `forall`s/`=>`s, -which makes `:print fmap` display as -`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected. - -Although ImpredicativeTypes is a somewhat unpredictable from a type inference -perspective, there is no danger in using it in the GHCi debugger, since all -of the terms that the GHCi debugger deals with have already been typechecked. --} diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs index ea682702c6..7bcb1a364c 100644 --- a/compiler/GHC/Runtime/Heap/Inspect.hs +++ b/compiler/GHC/Runtime/Heap/Inspect.hs @@ -559,11 +559,52 @@ trIO = liftTcM . liftIO liftTcM :: TcM a -> TR a liftTcM = id +-- When we make new unification variables in the GHCi debugger, +-- we use RuntimeUnkTvs. See Note [RuntimeUnkTv]. newVar :: Kind -> TR TcType -newVar = liftTcM . newFlexiTyVarTy +newVar kind = liftTcM (do { tv <- newAnonMetaTyVar RuntimeUnkTv kind + ; return (mkTyVarTy tv) }) newOpenVar :: TR TcType -newOpenVar = liftTcM newOpenFlexiTyVarTy +newOpenVar = liftTcM (do { kind <- newOpenTypeKind + ; newVar kind }) + +{- Note [RuntimeUnkTv] +~~~~~~~~~~~~~~~~~~~~~~ +In the GHCi debugger we use unification variables whose MetaInfo is +RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can +unify with a polytype (see GHC.Tc.Utils.Unify.metaTyVarUpdateOK). +If we don't do this `:print <term>` will fail if the type of <term> +has nested `forall`s or `=>`s. + +This is because the GHCi debugger's internals will attempt to unify a +metavariable with the type of <term> and then display the result, but +if the type has nested `forall`s or `=>`s, then unification will fail +unless we do something special. As a result, `:print` will bail out +and the unhelpful result will be `<term> = (_t1::t1)` (where `t1` is a +metavariable). + +Beware: <term> can have nested `forall`s even if its definition doesn't use +RankNTypes! Here is an example from #14828: + + class Functor f where + fmap :: (a -> b) -> f a -> f b + +Somewhat surprisingly, `:print fmap` considers the type of fmap to have +nested foralls. This is because the GHCi debugger sees the type +`fmap :: forall f. Functor f => forall a b. (a -> b) -> f a -> f b`. +We could envision deeply instantiating this type to get the type +`forall f a b. Functor f => (a -> b) -> f a -> f b`, +but this trick wouldn't work for higher-rank types. + +Instead, we adopt a simpler fix: allow RuntimeUnkTv to unify with a +polytype (specifically, see ghci_tv in GHC.Tc.Utils.Unify.preCheck). +This allows metavariables to unify with types that have +nested (or higher-rank) `forall`s/`=>`s, which makes `:print fmap` +display as +`fmap = (_t1::forall a b. Functor f => (a -> b) -> f a -> f b)`, as expected. +-} + instTyVars :: [TyVar] -> TR (TCvSubst, [TcTyVar]) -- Instantiate fresh mutable type variables from some TyVars @@ -578,6 +619,10 @@ type RttiInstantiation = [(TcTyVar, TyVar)] -- If the TcTyVar has not been refined by the runtime type -- elaboration, then we want to turn it back into the -- original RuntimeUnk + -- + -- July 20: I'm not convinced that the little dance from + -- RuntimeUnkTv unification variables to RuntimeUnk skolems + -- is buying us anything. ToDo: get rid of it. -- | Returns the instantiated type scheme ty', and the -- mapping from new (instantiated) -to- old (skolem) type variables @@ -585,6 +630,7 @@ instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation) instScheme (tvs, ty) = do { (subst, tvs') <- instTyVars tvs ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs] + ; traceTR (text "instScheme" <+> (ppr tvs $$ ppr ty $$ ppr tvs')) ; return (substTy subst ty, rtti_inst) } applyRevSubst :: RttiInstantiation -> TR () diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs index 3585c9ad70..400d4afbe7 100644 --- a/compiler/GHC/Tc/Deriv/Generate.hs +++ b/compiler/GHC/Tc/Deriv/Generate.hs @@ -1691,19 +1691,14 @@ a polytype. E.g. @(T x -> forall b. b -> b) op -The use of type applications is crucial here. If we had tried using only -explicit type signatures, like so: +The use of type applications is crucial here. We have to instantiate +both type args of (coerce :: Coercible a b => a -> b) to polytypes, +and we can only do that with VTA or Quick Look. Here VTA seems more +appropriate for machine generated code: it's simple and robust. - instance C <rep-ty> => C (T x) where - op :: T x -> forall b. b -> b - op = coerce (op :: <rep-ty> -> forall b. b -> b) - -Then GHC will attempt to deeply skolemize the two type signatures, which will -wreak havoc with the Coercible solver. Therefore, we instead use type -applications, which do not deeply skolemize and thus avoid this issue. -The downside is that we currently require -XImpredicativeTypes to permit this -polymorphic type instantiation, so we have to switch that flag on locally in -GHC.Tc.Deriv.genInst. See #8503 for more discussion. +However, to allow VTA with polytypes we must switch on +-XImpredicativeTypes locally in GHC.Tc.Deriv.genInst. +See #8503 for more discussion. Note [Newtype-deriving trickiness] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1807,9 +1802,8 @@ break this example (from the T15290d test case): c = coerce @(Int -> forall b. b -> Int) c -That is because the instance signature deeply skolemizes the forall-bound -`b`, which wreaks havoc with the `Coercible` solver. An additional visible type -argument of @(Int -> forall b. b -> Age) is enough to prevent this. +That is because we still need to instantiate the second argument of +coerce with a polytype, and we can only do that with VTA or QuickLook. Be aware that the use of an instance signature doesn't /solve/ this problem; it just makes it less likely to occur. For example, if a class has diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs new file mode 100644 index 0000000000..79749c70c7 --- /dev/null +++ b/compiler/GHC/Tc/Gen/App.hs @@ -0,0 +1,1083 @@ +{- +% +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +-} + +{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow] + +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} + +module GHC.Tc.Gen.App + ( tcApp + , tcInferSigma + , tcValArg + , tcExprPrag ) where + +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC ) + +import GHC.Tc.Gen.Head +import GHC.Hs +import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.Unify +import GHC.Tc.Utils.Instantiate +import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe ) +import GHC.Tc.Gen.HsType +import GHC.Tc.Utils.TcMType +import GHC.Tc.Types.Origin +import GHC.Tc.Utils.TcType as TcType +import GHC.Core.TyCon +import GHC.Core.TyCo.Rep +import GHC.Core.TyCo.Ppr +import GHC.Core.TyCo.Subst (substTyWithInScope) +import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType ) +import GHC.Core.Type +import GHC.Tc.Types.Evidence +import GHC.Types.Var.Set +import GHC.Builtin.PrimOps( tagToEnumKey ) +import GHC.Builtin.Names +import GHC.Driver.Session +import GHC.Types.SrcLoc +import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet ) +import GHC.Data.Maybe +import GHC.Utils.Misc +import GHC.Utils.Outputable as Outputable +import GHC.Utils.Panic +import qualified GHC.LanguageExtensions as LangExt + +import Control.Monad +import Data.Function + +#include "HsVersions.h" + +import GHC.Prelude + +{- ********************************************************************* +* * + Quick Look overview +* * +********************************************************************* -} + +{- Note [Quick Look] +~~~~~~~~~~~~~~~~~~~~ +The implementation of Quick Look closely follows the QL paper + A quick look at impredicativity, Serrano et al, ICFP 2020 + https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/ + +All the moving parts are in this module, GHC.Tc.Gen.App, so named +because it deal with n-ary application. The main workhorse is tcApp. + +Some notes relative to the paper + +* The "instantiation variables" of the paper are ordinary unification + variables. We keep track of which variables are instantiation variables + by keeping a set Delta of instantiation variables. + +* When we learn what an instantiation variable must be, we simply unify + it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2) + of the paper. This may fill in a (mutable) instantiation variable with + a polytype. + +* When QL is done, we don't need to turn the un-filled-in + instantiation variables into unification variables -- they already + are! + + Moreover, all filled-in occurrences of instantiation variables + have been zonked away (see "Crucial step" in tcValArgs), and + so the rest of the type checker never sees a meta-type variable + filled in with a polytype. For the rest of the typechecker, + a meta type variable stands (only) for a monotype. + +* We cleverly avoid the quadratic cost of QL, alluded to in the paper. + See Note [Quick Look at value arguments] +-} + + +{- ********************************************************************* +* * + tcInferSigma +* * +********************************************************************* -} + +tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType +-- Used only to implement :type; see GHC.Tc.Module.tcRnExpr +-- True <=> instantiate -- return a rho-type +-- False <=> don't instantiate -- return a sigma-type +tcInferSigma inst (L loc rn_expr) + | (rn_fun, rn_args, _) <- splitHsApps rn_expr + = addExprCtxt rn_expr $ + setSrcSpan loc $ + do { do_ql <- wantQuickLook rn_fun + ; (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args Nothing + ; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst rn_fun fun_sigma rn_args + ; _tc_args <- tcValArgs do_ql tc_fun inst_args + ; return app_res_sigma } + +{- ********************************************************************* +* * + Typechecking n-ary applications +* * +********************************************************************* -} + +{- Note [Application chains and heads] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Quick Look treats application chains specially. What is an +"application chain"? See Fig 2, of the QL paper: "A quick look at +impredicativity" (ICFP'20). Here's the syntax: + +app :: head + | app expr -- HsApp: ordinary application + | app @type -- HsTypeApp: VTA + | expr `head` expr -- OpApp: infix applications + | ( app ) -- HsPar: parens + | {-# PRAGMA #-} app -- HsPragE: pragmas + +head ::= f -- HsVar: variables + | fld -- HsRecFld: record field selectors + | (expr :: ty) -- ExprWithTySig: expr with user type sig + | other_expr -- Other expressions + +When tcExpr sees something that starts an application chain (namely, +any of the constructors in 'app' or 'head'), it invokes tcApp to +typecheck it: see Note [tcApp: typechecking applications]. However, +for HsPar and HsPragE, there is no tcWrapResult (which would +instantiate types, bypassing Quick Look), so nothing is gained by +using the application chain route, and we can just recurse to tcExpr. + +A "head" has three special cases (for which we can infer a polytype +using tcInferAppHead_maybe); otherwise is just any old expression (for +which we can infer a rho-type (via tcInfer). + +There is no special treatment for HsUnboundVar, HsOverLit etc, because +we can't get a polytype from them. + +Left and right sections (e.g. (x +) and (+ x)) are not yet supported. +Probably left sections (x +) would be esay to add, since x is the +first arg of (+); but right sections are not so easy. For symmetry +reasons I've left both unchanged, in GHC.Tc.Gen.Expr. + +It may not be immediately obvious why ExprWithTySig (e::ty) should be +dealt with by tcApp, even when it is not applied to anything. Consider + f :: [forall a. a->a] -> Int + ...(f (undefined :: forall b. b))... +Clearly this should work! But it will /only/ work because if we +instantiate that (forall b. b) impredicatively! And that only happens +in tcApp. + +Note [tcApp: typechecking applications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tcApp implements the APP-Downarrow/Uparrow rule of +Fig 3, plus the modification in Fig 5, of the QL paper: +"A quick look at impredicativity" (ICFP'20). + +It treats application chains (f e1 @ty e2) specially: + +* So we can report errors like "in the third arument of a call of f" + +* So we can do Visible Type Application (VTA), for which we must not + eagerly instantiate the function part of the application. + +* So that we can do Quick Look impredicativity. + +tcApp works like this: + +1. Use splitHsApps, which peels off + HsApp, HsTypeApp, HsPrag, HsPar + returning the function in the corner and the arguments + + splitHsApps can deal with infix as well as prefix application, + and returns a Rebuilder to re-assemble the the application after + typechecking. + + The "list of arguments" is [HsExprArg], described in Note [HsExprArg]. + in GHC.Tc.Gen.Head + +2. Use tcInferAppHead to infer the type of the fuction, + as an (uninstantiated) TcSigmaType + There are special cases for + HsVar, HsRecFld, and ExprWithTySig + Otherwise, delegate back to tcExpr, which + infers an (instantiated) TcRhoType + +3. Use tcInstFun to instantiate the function, Quick-Looking as we go. + This implements the |-inst judgement in Fig 4, plus the + modification in Fig 5, of the QL paper: + "A quick look at impredicativity" (ICFP'20). + + In tcInstFun we take a quick look at value arguments, using + quickLookArg. See Note [Quick Look at value arguments]. + +4. Use quickLookResultType to take a quick look at the result type, + when in checking mode. This is the shaded part of APP-Downarrow + in Fig 5. + +5. Use tcValArgs to typecheck the value arguments + +6. After a gruesome special case for tagToEnum, rebuild the result. + + +Some cases that /won't/ work: + +1. Consider this (which uses visible type application): + + (let { f :: forall a. a -> a; f x = x } in f) @Int + + Since 'let' is not among the special cases for tcInferAppHead, + we'll delegate back to tcExpr, which will instantiate f's type + and the type application to @Int will fail. Too bad! + +-} + +tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) +-- See Note [tcApp: typechecking applications] +tcApp rn_expr exp_res_ty + | (rn_fun, rn_args, rebuild) <- splitHsApps rn_expr + = do { (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args + (checkingExpType_maybe exp_res_ty) + + -- Instantiate + ; do_ql <- wantQuickLook rn_fun + ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True rn_fun fun_sigma rn_args + + -- Quick look at result + ; quickLookResultType do_ql delta app_res_rho exp_res_ty + + ; whenDOptM Opt_D_dump_tc_trace $ + do { inst_args <- mapM zonkArg inst_args -- Only when tracing + ; traceTc "tcApp" (vcat [ text "rn_fun" <+> ppr rn_fun + , text "inst_args" <+> brackets (pprWithCommas pprHsExprArgTc inst_args) + , text "do_ql: " <+> ppr do_ql + , text "fun_sigma: " <+> ppr fun_sigma + , text "delta: " <+> ppr delta + , text "app_res_rho:" <+> ppr app_res_rho + , text "exp_res_ty:" <+> ppr exp_res_ty + , text "rn_expr:" <+> ppr rn_expr ]) } + + -- Typecheck the value arguments + ; tc_args <- tcValArgs do_ql tc_fun inst_args + + -- Special case for tagToEnum# + ; if isTagToEnum rn_fun + then tcTagToEnum rn_expr tc_fun tc_args app_res_rho exp_res_ty + else + + do { -- Reconstruct + ; let tc_expr = rebuild tc_fun tc_args + + -- Wrap the result + -- NB: app_res_ty may be a polytype, via zonkQuickLook + ; addFunResCtxt tc_fun tc_args app_res_rho exp_res_ty $ + tcWrapResult rn_expr tc_expr app_res_rho exp_res_ty } } + +-------------------- +-- zonkArg is used *only* during debug-tracing, to make it easier to +-- see what is going on. For that reason, it is not a full zonk: add +-- more if you need it. +zonkArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst) +zonkArg eva@(EValArg { eva_arg_ty = Scaled m ty }) + = do { ty' <- zonkTcType ty + ; return (eva { eva_arg_ty = Scaled m ty' }) } +zonkArg arg = return arg + + +wantQuickLook :: HsExpr GhcRn -> TcM Bool +-- GHC switches on impredicativity all the time for ($) +wantQuickLook (HsVar _ f) | unLoc f `hasKey` dollarIdKey = return True +wantQuickLook _ = xoptM LangExt.ImpredicativeTypes + + +---------------- +tcValArgs :: Bool -- Quick-look on? + -> HsExpr GhcTc -- The function (for error messages) + -> [HsExprArg 'TcpInst] -- Actual argument + -> TcM [HsExprArg 'TcpTc] -- Resulting argument +tcValArgs quick_look fun args + = go 1 args + where + go _ [] = return [] + go n (arg:args) = do { (n',arg') <- tc_arg n arg + ; args' <- go n' args + ; return (arg' : args') } + + tc_arg :: Int -> HsExprArg 'TcpInst -> TcM (Int, HsExprArg 'TcpTc) + tc_arg n (EPar l) = return (n, EPar l) + tc_arg n (EPrag l p) = return (n, EPrag l (tcExprPrag p)) + tc_arg n (EWrap wrap) = return (n, EWrap wrap) + tc_arg n (ETypeArg l hs_ty ty) = return (n+1, ETypeArg l hs_ty ty) + + tc_arg n eva@(EValArg { eva_arg = arg, eva_arg_ty = Scaled mult arg_ty }) + = do { -- Crucial step: expose QL results before checking arg_ty + -- So far as the paper is concerned, this step applies + -- the poly-substitution Theta, learned by QL, so that we + -- "see" the polymorphism in that argument type. E.g. + -- (:) e ids, where ids :: [forall a. a->a] + -- (:) :: forall p. p->[p]->[p] + -- Then Theta = [p :-> forall a. a->a], and we want + -- to check 'e' with expected type (forall a. a->a) + arg_ty <- if quick_look then zonkTcType arg_ty + else return arg_ty + + -- Now check the argument + ; arg' <- addErrCtxt (funAppCtxt fun (eValArgExpr arg) n) $ + tcScalingUsage mult $ + do { traceTc "tcEValArg" $ + vcat [ ppr n <+> text "of" <+> ppr fun + , text "arg type:" <+> ppr arg_ty + , text "arg:" <+> ppr arg ] + ; tcEValArg arg arg_ty } + + ; return (n+1, eva { eva_arg = ValArg arg' + , eva_arg_ty = Scaled mult arg_ty }) } + +tcEValArg :: EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc) +-- Typecheck one value argument of a function call +tcEValArg (ValArg arg) exp_arg_sigma + = tcCheckPolyExprNC arg exp_arg_sigma + +tcEValArg (ValArgQL { va_expr = L loc _, va_fun = fun, va_args = args + , va_ty = app_res_rho, va_rebuild = rebuild }) exp_arg_sigma + = setSrcSpan loc $ + do { traceTc "tcEValArg {" (vcat [ ppr fun <+> ppr args ]) + ; tc_args <- tcValArgs True fun args + ; co <- unifyType Nothing app_res_rho exp_arg_sigma + ; traceTc "tcEValArg }" empty + ; return (L loc $ mkHsWrapCo co $ rebuild fun tc_args) } + +---------------- +tcValArg :: HsExpr GhcRn -- The function (for error messages) + -> LHsExpr GhcRn -- Actual argument + -> Scaled TcSigmaType -- expected arg type + -> Int -- # of argument + -> TcM (LHsExpr GhcTc) -- Resulting argument +-- tcValArg is called only from Gen.Expr, dealing with left and right sections +tcValArg fun arg (Scaled mult arg_ty) arg_no + = addErrCtxt (funAppCtxt fun arg arg_no) $ + tcScalingUsage mult $ + do { traceTc "tcValArg" $ + vcat [ ppr arg_no <+> text "of" <+> ppr fun + , text "arg type:" <+> ppr arg_ty + , text "arg:" <+> ppr arg ] + ; tcCheckPolyExprNC arg arg_ty } + + +{- ********************************************************************* +* * + Instantiating the call +* * +********************************************************************* -} + +type Delta = TcTyVarSet -- Set of instantiation variables, + -- written \kappa in the QL paper + -- Just a set of ordinary unification variables, + -- but ones that QL may fill in with polytypes + +tcInstFun :: Bool -- True <=> Do quick-look + -> Bool -- False <=> Instantiate only /inferred/ variables at the end + -- so may return a sigma-typex + -- True <=> Instantiate all type variables at the end: + -- return a rho-type + -- The /only/ call site that passes in False is the one + -- in tcInferSigma, which is used only to implement :type + -- Otherwise we do eager instantiation; in Fig 5 of the paper + -- |-inst returns a rho-type + -> HsExpr GhcRn -> TcSigmaType -> [HsExprArg 'TcpRn] + -> TcM ( Delta + , [HsExprArg 'TcpInst] + , TcSigmaType ) +-- This function implements the |-inst judgement in Fig 4, plus the +-- modification in Fig 5, of the QL paper: +-- "A quick look at impredicativity" (ICFP'20). +tcInstFun do_ql inst_final rn_fun fun_sigma rn_args + = do { traceTc "tcInstFun" (ppr rn_fun $$ ppr rn_args $$ text "do_ql" <+> ppr do_ql) + ; go emptyVarSet [] [] fun_sigma rn_args } + where + fun_orig = exprCtOrigin rn_fun + herald = sep [ text "The function" <+> quotes (ppr rn_fun) + , text "is applied to"] + + -- Count value args only when complaining about a function + -- applied to too many value args + -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify. + n_val_args = count isHsValArg rn_args + + fun_is_out_of_scope -- See Note [VTA for out-of-scope functions] + = case rn_fun of + HsUnboundVar {} -> True + _ -> False + + inst_all :: ArgFlag -> Bool + inst_all (Invisible {}) = True + inst_all Required = False + + inst_inferred :: ArgFlag -> Bool + inst_inferred (Invisible InferredSpec) = True + inst_inferred (Invisible SpecifiedSpec) = False + inst_inferred Required = False + + inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool + inst_fun [] | inst_final = inst_all + | otherwise = inst_inferred + inst_fun (EValArg {} : _) = inst_all + inst_fun _ = inst_inferred + + ----------- + go, go1 :: Delta + -> [HsExprArg 'TcpInst] -- Accumulator, reversed + -> [Scaled TcSigmaType] -- Value args to which applied so far + -> TcSigmaType -> [HsExprArg 'TcpRn] + -> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType) + + -- go: If fun_ty=kappa, look it up in Theta + go delta acc so_far fun_ty args + | Just kappa <- tcGetTyVar_maybe fun_ty + , kappa `elemVarSet` delta + = do { cts <- readMetaTyVar kappa + ; case cts of + Indirect fun_ty' -> go delta acc so_far fun_ty' args + Flexi -> go1 delta acc so_far fun_ty args } + | otherwise + = go1 delta acc so_far fun_ty args + + -- go1: fun_ty is not filled-in instantiation variable + -- ('go' dealt with that case) + + -- Rule IALL from Fig 4 of the QL paper + go1 delta acc so_far fun_ty args + | (tvs, body1) <- tcSplitSomeForAllTys (inst_fun args) fun_ty + , (theta, body2) <- tcSplitPhiTy body1 + , not (null tvs && null theta) + = do { (inst_tvs, wrap, fun_rho) <- setSrcSpanFromArgs rn_args $ + instantiateSigma fun_orig tvs theta body2 + -- setSrcSpanFromArgs: important for the class constraints + -- that may be emitted from instantiating fun_sigma + ; go (delta `extendVarSetList` inst_tvs) + (addArgWrap wrap acc) so_far fun_rho args } + -- Going around again means we deal easily with + -- nested forall a. Eq a => forall b. Show b => blah + + -- Rule IRESULT from Fig 4 of the QL paper + go1 delta acc _ fun_ty [] + = do { traceTc "tcInstFun:ret" (ppr fun_ty) + ; return (delta, reverse acc, fun_ty) } + + go1 delta acc so_far fun_ty (EPar sp : args) + = go1 delta (EPar sp : acc) so_far fun_ty args + + go1 delta acc so_far fun_ty (EPrag sp prag : args) + = go1 delta (EPrag sp prag : acc) so_far fun_ty args + + -- Rule ITYARG from Fig 4 of the QL paper + go1 delta acc so_far fun_ty ( ETypeArg { eva_loc = loc, eva_hs_ty = hs_ty } + : rest_args ) + | fun_is_out_of_scope -- See Note [VTA for out-of-scope functions] + = go delta acc so_far fun_ty rest_args + + | otherwise + = do { (ty_arg, inst_ty) <- tcVTA fun_ty hs_ty + ; let arg' = ETypeArg { eva_loc = loc, eva_hs_ty = hs_ty, eva_ty = ty_arg } + ; go delta (arg' : acc) so_far inst_ty rest_args } + + -- Rule IVAR from Fig 4 of the QL paper: + go1 delta acc so_far fun_ty args@(EValArg {} : _) + | Just kappa <- tcGetTyVar_maybe fun_ty + , kappa `elemVarSet` delta + = -- Function type was of form f :: forall a b. t1 -> t2 -> b + -- with 'b', one of the quantified type variables, in the corner + -- but the call applies it to three or more value args. + -- Suppose b is instantiated by kappa. Then we want to make fresh + -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2 + -- + -- In principle what is happening here is not unlike matchActualFunTysRho + -- but there are many small differences: + -- - We know that the function type in unfilled meta-tyvar + -- matchActualFunTysRho is much more general, has a loop, etc. + -- - We must be sure to actually update the variable right now, + -- not defer in any way, because this is a QL instantiation variable. + -- - We need the freshly allocated unification variables, to extend + -- delta with. + -- It's easier just to do the job directly here. + do { arg_nus <- replicateM (countLeadingValArgs args) newOpenFlexiTyVar + ; res_nu <- newOpenFlexiTyVar + ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa) + ; let delta' = delta `extendVarSetList` (res_nu:arg_nus) + arg_tys = mkTyVarTys arg_nus + res_ty = mkTyVarTy res_nu + fun_ty' = mkVisFunTysMany arg_tys res_ty + co_wrap = mkWpCastN (mkTcGReflLeftCo Nominal fun_ty' kind_co) + acc' = addArgWrap co_wrap acc + -- Suppose kappa :: kk + -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk + -- co_wrap :: (fun_ty' |> kind_co) ~ fun_ty' + ; writeMetaTyVar kappa (mkCastTy fun_ty' kind_co) + -- kappa is uninstantiated ('go' already checked that) + ; go delta' acc' so_far fun_ty' args } + + -- Rule IARG from Fig 4 of the QL paper: + go1 delta acc so_far fun_ty + (eva@(EValArg { eva_arg = ValArg arg }) : rest_args) + = do { (wrap, arg_ty, res_ty) <- matchActualFunTySigma herald + (Just (ppr rn_fun)) + (n_val_args, so_far) fun_ty + ; let arg_no = 1 + count isVisibleArg acc + -- We could cache this in a pair with acc; but + -- it's only evaluated if there's a type error + ; (delta', arg') <- if do_ql + then addErrCtxt (funAppCtxt rn_fun arg arg_no) $ + -- Context needed for constraints + -- generated by calls in arg + quickLookArg delta arg arg_ty + else return (delta, ValArg arg) + ; let acc' = eva { eva_arg = arg', eva_arg_ty = arg_ty } + : addArgWrap wrap acc + ; go delta' acc' (arg_ty:so_far) res_ty rest_args } + + + +{- ********************************************************************* +* * + Visible type application +* * +********************************************************************* -} + +tcVTA :: TcType -- Function type + -> LHsWcType GhcRn -- Argument type + -> TcM (TcType, TcType) +-- Deal with a visible type application +-- The function type has already had its Inferred binders instantiated +tcVTA fun_ty hs_ty + | Just (tvb, inner_ty) <- tcSplitForAllTy_maybe fun_ty + , binderArgFlag tvb == Specified + -- It really can't be Inferred, because we've just + -- instantiated those. But, oddly, it might just be Required. + -- See Note [Required quantifiers in the type of a term] + = do { let tv = binderVar tvb + kind = tyVarKind tv + ; ty_arg <- tcHsTypeApp hs_ty kind + + ; inner_ty <- zonkTcType inner_ty + -- See Note [Visible type application zonk] + + ; let in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg]) + insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty + -- NB: tv and ty_arg have the same kind, so this + -- substitution is kind-respecting + ; traceTc "VTA" (vcat [ppr tv, debugPprType kind + , debugPprType ty_arg + , debugPprType (tcTypeKind ty_arg) + , debugPprType inner_ty + , debugPprType insted_ty ]) + ; return (ty_arg, insted_ty) } + + | otherwise + = do { (_, fun_ty) <- zonkTidyTcType emptyTidyEnv fun_ty + ; failWith $ + text "Cannot apply expression of type" <+> quotes (ppr fun_ty) $$ + text "to a visible type argument" <+> quotes (ppr hs_ty) } + +{- Note [Required quantifiers in the type of a term] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#15859) + + data A k :: k -> Type -- A :: forall k -> k -> Type + type KindOf (a :: k) = k -- KindOf :: forall k. k -> Type + a = (undefind :: KindOf A) @Int + +With ImpredicativeTypes (thin ice, I know), we instantiate +KindOf at type (forall k -> k -> Type), so + KindOf A = forall k -> k -> Type +whose first argument is Required + +We want to reject this type application to Int, but in earlier +GHCs we had an ASSERT that Required could not occur here. + +The ice is thin; c.f. Note [No Required TyCoBinder in terms] +in GHC.Core.TyCo.Rep. + +Note [VTA for out-of-scope functions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose 'wurble' is not in scope, and we have + (wurble @Int @Bool True 'x') + +Then the renamer will make (HsUnboundVar "wurble) for 'wurble', +and the typechecker will typecheck it with tcUnboundId, giving it +a type 'alpha', and emitting a deferred Hole constraint, to +be reported later. + +But then comes the visible type application. If we do nothing, we'll +generate an immediate failure (in tc_app_err), saying that a function +of type 'alpha' can't be applied to Bool. That's insane! And indeed +users complain bitterly (#13834, #17150.) + +The right error is the Hole, which has /already/ been emitted by +tcUnboundId. It later reports 'wurble' as out of scope, and tries to +give its type. + +Fortunately in tcInstFun we still have access to the function, so we +can check if it is a HsUnboundVar. We use this info to simply skip +over any visible type arguments. We've already inferred the type of +the function (in tcInferAppHead), so we'll /already/ have emitted a +Hole constraint; failing preserves that constraint. + +We do /not/ want to fail altogether in this case (via failM) becuase +that may abandon an entire instance decl, which (in the presence of +-fdefer-type-errors) leads to leading to #17792. + +Downside; the typechecked term has lost its visible type arguments; we +don't even kind-check them. But let's jump that bridge if we come to +it. Meanwhile, let's not crash! + + +Note [Visible type application zonk] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg). + +* tcHsTypeApp only guarantees that + - ty_arg is zonked + - kind(zonk(tv)) = kind(ty_arg) + (checkExpectedKind zonks as it goes). + +So we must zonk inner_ty as well, to guarantee consistency between zonk(tv) +and inner_ty. Otherwise we can build an ill-kinded type. An example was +#14158, where we had: + id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a +and we had the visible type application + id @(->) + +* We instantiated k := kappa, yielding + forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a +* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *). +* That instantiated (->) as ((->) q1 q1), and unified kappa := q1, + Here q1 :: RuntimeRep +* Now we substitute + cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> * + but we must first zonk the inner_ty to get + forall (a :: TYPE q1). cat a a + so that the result of substitution is well-kinded + Failing to do so led to #14158. + +-} + +{- ********************************************************************* +* * + Quick Look +* * +********************************************************************* -} + +{- Note [Quick Look at value arguments] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function quickLookArg implements the "QL argument" judgement of +the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020), +rather directly. + +Wrinkles: + +* We avoid zonking, so quickLookArg thereby sees the argument type /before/ + the QL substitution Theta is applied to it. So we achieve argument-order + independence for free (see 5.7 in the paper). + +* When we quick-look at an argument, we save the work done, by returning + an EValArg with a ValArgQL inside it. (It started life with a ValArg + inside.) The ValArgQL remembers all the work that QL did (notably, + decomposing the argument and instantiating) so that tcValArgs does + not need to repeat it. Rather neat, and remarkably easy. +-} + +---------------- +quickLookArg :: Delta + -> LHsExpr GhcRn -- Argument + -> Scaled TcSigmaType -- Type expected by the function + -> TcM (Delta, EValArg 'TcpInst) +-- See Note [Quick Look at value arguments] +-- +-- The returned Delta is a superset of the one passed in +-- with added instantiation variables from +-- (a) the call itself +-- (b) the arguments of the call +quickLookArg delta larg (Scaled _ arg_ty) + | isEmptyVarSet delta = skipQuickLook delta larg + | otherwise = go arg_ty + where + guarded = isGuardedTy arg_ty + -- NB: guardedness is computed based on the original, + -- unzonked arg_ty, so we deliberately do not exploit + -- guardedness that emerges a result of QL on earlier args + + go arg_ty | not (isRhoTy arg_ty) + = skipQuickLook delta larg + + -- This top-level zonk step, which is the reason + -- we need a local 'go' loop, is subtle + -- See Section 9 of the QL paper + | Just kappa <- tcGetTyVar_maybe arg_ty + , kappa `elemVarSet` delta + = do { info <- readMetaTyVar kappa + ; case info of + Indirect arg_ty' -> go arg_ty' + Flexi -> quickLookArg1 guarded delta larg arg_ty } + + | otherwise + = quickLookArg1 guarded delta larg arg_ty + +isGuardedTy :: TcType -> Bool +isGuardedTy ty + | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal + | Just {} <- tcSplitAppTy_maybe ty = True + | otherwise = False + +quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType + -> TcM (Delta, EValArg 'TcpInst) +quickLookArg1 guarded delta larg@(L loc arg) arg_ty + = setSrcSpan loc $ + do { let (rn_fun,rn_args,rebuild) = splitHsApps arg + ; mb_fun_ty <- tcInferAppHead_maybe rn_fun rn_args (Just arg_ty) + ; traceTc "quickLookArg 1" $ + vcat [ text "arg:" <+> ppr arg + , text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty + , text "args:" <+> ppr rn_args ] + + ; case mb_fun_ty of { + Nothing -> -- fun is too complicated + skipQuickLook delta larg ; + Just (fun', fun_sigma) -> + + do { let no_free_kappas = findNoQuantVars fun_sigma rn_args + ; traceTc "quickLookArg 2" $ + vcat [ text "no_free_kappas:" <+> ppr no_free_kappas + , text "guarded:" <+> ppr guarded ] + ; if not (guarded || no_free_kappas) + then skipQuickLook delta larg + else + do { do_ql <- wantQuickLook rn_fun + ; (delta_app, inst_args, app_res_rho) + <- tcInstFun do_ql True rn_fun fun_sigma rn_args + ; traceTc "quickLookArg" $ + vcat [ text "arg:" <+> ppr arg + , text "delta:" <+> ppr delta + , text "delta_app:" <+> ppr delta_app + , text "arg_ty:" <+> ppr arg_ty + , text "app_res_rho:" <+> ppr app_res_rho ] + + -- Do quick-look unification + -- NB: arg_ty may not be zonked, but that's ok + ; let delta' = delta `unionVarSet` delta_app + ; qlUnify delta' arg_ty app_res_rho + + ; let ql_arg = ValArgQL { va_expr = larg, va_fun = fun' + , va_args = inst_args + , va_ty = app_res_rho + , va_rebuild = rebuild } + ; return (delta', ql_arg) } } } } + +skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst) +skipQuickLook delta larg = return (delta, ValArg larg) + +---------------- +quickLookResultType :: Bool -> Delta -> TcRhoType -> ExpRhoType -> TcM () +-- This function implements the shaded bit of rule APP-Downarrow in +-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20). + +quickLookResultType do_ql delta app_res_rho exp_res_ty + | do_ql + , not (isEmptyVarSet delta) -- Optimisation only + , Just exp_rho <- checkingExpType_maybe exp_res_ty + -- In checking mode only + = qlUnify delta app_res_rho exp_rho + | otherwise + = return () + +--------------------- +qlUnify :: Delta -> TcType -> TcType -> TcM () +-- Unify ty1 with ty2, unifying only variables in delta +qlUnify delta ty1 ty2 + = do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2) + ; go (emptyVarSet,emptyVarSet) ty1 ty2 } + where + go :: (TyVarSet, TcTyVarSet) + -> TcType -> TcType + -> TcM () + -- The TyVarSets give the variables bound by enclosing foralls + -- for the corresponding type. Don't unify with these. + go bvs (TyVarTy tv) ty2 + | tv `elemVarSet` delta = go_kappa bvs tv ty2 + + go (bvs1, bvs2) ty1 (TyVarTy tv) + | tv `elemVarSet` delta = go_kappa (bvs2,bvs1) tv ty1 + + go bvs (CastTy ty1 _) ty2 = go bvs ty1 ty2 + go bvs ty1 (CastTy ty2 _) = go bvs ty1 ty2 + + go _ (TyConApp tc1 []) (TyConApp tc2 []) + | tc1 == tc2 -- See GHC.Tc.Utils.Unify + = return () -- Note [Expanding synonyms during unification] + + -- Now, and only now, expand synonyms + go bvs rho1 rho2 + | Just rho1 <- tcView rho1 = go bvs rho1 rho2 + | Just rho2 <- tcView rho2 = go bvs rho1 rho2 + + go bvs (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | tc1 == tc2 + , not (isTypeFamilyTyCon tc1) + , tys1 `equalLength` tys2 + = zipWithM_ (go bvs) tys1 tys2 + + -- Decompose (arg1 -> res1) ~ (arg2 -> res2) + -- and (c1 => res1) ~ (c2 => res2) + -- But for the latter we only learn instantiation info from t1~t2 + -- We look at the multiplicity too, although the chances of getting + -- impredicative instantiation info from there seems...remote. + go bvs (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 }) + (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 }) + | af1 == af2 + = do { when (af1 == VisArg) $ + do { go bvs arg1 arg2; go bvs mult1 mult2 } + ; go bvs res1 res2 } + + -- ToDo: c.f. Tc.Utils.unify.uType, + -- which does not split FunTy here + -- Also NB tcRepSplitAppTy here, which does not split (c => t) + go bvs (AppTy t1a t1b) ty2 + | Just (t2a, t2b) <- tcRepSplitAppTy_maybe ty2 + = do { go bvs t1a t2a; go bvs t1b t2b } + + go bvs ty1 (AppTy t2a t2b) + | Just (t1a, t1b) <- tcRepSplitAppTy_maybe ty1 + = do { go bvs t1a t2a; go bvs t1b t2b } + + go (bvs1, bvs2) (ForAllTy bv1 ty1) (ForAllTy bv2 ty2) + = go (bvs1',bvs2') ty1 ty2 + where + bvs1' = bvs1 `extendVarSet` binderVar bv1 + bvs2' = bvs2 `extendVarSet` binderVar bv2 + + go _ _ _ = return () + + + ---------------- + go_kappa bvs kappa ty2 + = ASSERT2( isMetaTyVar kappa, ppr kappa ) + do { info <- readMetaTyVar kappa + ; case info of + Indirect ty1 -> go bvs ty1 ty2 + Flexi -> do { ty2 <- zonkTcType ty2 + ; go_flexi bvs kappa ty2 } } + + ---------------- + go_flexi (_,bvs2) kappa ty2 -- ty2 is zonked + | -- See Note [Actual unification in qlUnify] + let ty2_tvs = shallowTyCoVarsOfType ty2 + , not (ty2_tvs `intersectsVarSet` bvs2) + -- Can't instantiate a delta-varto a forall-bound variable + , Just ty2 <- occCheckExpand [kappa] ty2 + -- Passes the occurs check + = do { let ty2_kind = typeKind ty2 + kappa_kind = tyVarKind kappa + ; co <- unifyKind (Just (ppr ty2)) ty2_kind kappa_kind + -- unifyKind: see Note [Actual unification in qlUnify] + + ; traceTc "qlUnify:update" $ + vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind) + 2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind) + , text "co:" <+> ppr co ] + ; writeMetaTyVar kappa (mkCastTy ty2 co) } + + | otherwise + = return () -- Occurs-check or forall-bound varialbe + + +{- Note [Actual unification in qlUnify] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty. +That is the entire point of qlUnify! Wrinkles: + +* We must not unify with anything bound by an enclosing forall; e.g. + (forall a. kappa -> Int) ~ forall a. a -> Int) + That's tracked by the 'bvs' arg of 'go'. + +* We must not make an occurs-check; we use occCheckExpand for that. + +* metaTyVarUpdateOK also checks for various other things, including + - foralls, and predicate types (which we want to allow here) + - type families (relates to a very specific and exotic performance + question, that is unlikely to bite here) + - blocking coercion holes + After some thought we believe that none of these are relevant + here + +* What if kappa and ty have different kinds? We solve that problem by + calling unifyKind, producing a coercion perhaps emitting some deferred + equality constraints. That is /different/ from the approach we use in + the main constraint solver for herterogeneous equalities; see Note + [Equalities with incompatible kinds] in Solver.Canonical + + Why different? Because: + - We can't use qlUnify to solve the kind constraint because qlUnify + won't unify ordinary (non-instantiation) unification variables. + (It would have to worry about lots of things like untouchability + if it did.) + - qlUnify can't give up if the kinds look un-equal because that would + mean that it might succeed some times (when the eager unifier + has already unified those kinds) but not others -- order + dependence. + - We can't use the ordinary unifier/constraint solver instead, + because it doesn't unify polykinds, and has all kinds of other + magic. qlUnify is very focused. + + TL;DR Calling unifyKind seems like the lesser evil. + -} + +{- ********************************************************************* +* * + Guardedness +* * +********************************************************************* -} + +findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool +-- True <=> there are no free quantified variables +-- in the result of the call +-- E.g. in the call (f e1 e2), if +-- f :: forall a b. a -> b -> Int return True +-- f :: forall a b. a -> b -> b return False (b is free) +findNoQuantVars fun_ty args + = go emptyVarSet fun_ty args + where + need_instantiation [] = True + need_instantiation (EValArg {} : _) = True + need_instantiation _ = False + + go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool + go bvs fun_ty args + | need_instantiation args + , (tvs, theta, rho) <- tcSplitSigmaTy fun_ty + , not (null tvs && null theta) + = go (bvs `extendVarSetList` tvs) rho args + + go bvs fun_ty [] = tyCoVarsOfType fun_ty `disjointVarSet` bvs + + go bvs fun_ty (EPar {} : args) = go bvs fun_ty args + go bvs fun_ty (EPrag {} : args) = go bvs fun_ty args + + go bvs fun_ty args@(ETypeArg {} : rest_args) + | (tvs, body1) <- tcSplitSomeForAllTys (== Inferred) fun_ty + , (theta, body2) <- tcSplitPhiTy body1 + , not (null tvs && null theta) + = go (bvs `extendVarSetList` tvs) body2 args + | Just (_tv, res_ty) <- tcSplitForAllTy_maybe fun_ty + = go bvs res_ty rest_args + | otherwise + = False -- E.g. head ids @Int + + go bvs fun_ty (EValArg {} : rest_args) + | Just (_, res_ty) <- tcSplitFunTy_maybe fun_ty + = go bvs res_ty rest_args + | otherwise + = False -- E.g. head id 'x' + + +{- ********************************************************************* +* * + tagToEnum# +* * +********************************************************************* -} + +{- Note [tagToEnum#] +~~~~~~~~~~~~~~~~~~~~ +Nasty check to ensure that tagToEnum# is applied to a type that is an +enumeration TyCon. Unification may refine the type later, but this +check won't see that, alas. It's crude, because it relies on our +knowing *now* that the type is ok, which in turn relies on the +eager-unification part of the type checker pushing enough information +here. In theory the Right Thing to do is to have a new form of +constraint but I definitely cannot face that! And it works ok as-is. + +Here's are two cases that should fail + f :: forall a. a + f = tagToEnum# 0 -- Can't do tagToEnum# at a type variable + + g :: Int + g = tagToEnum# 0 -- Int is not an enumeration + +When data type families are involved it's a bit more complicated. + data family F a + data instance F [Int] = A | B | C +Then we want to generate something like + tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int] +Usually that coercion is hidden inside the wrappers for +constructors of F [Int] but here we have to do it explicitly. + +It's all grotesquely complicated. +-} + +isTagToEnum :: HsExpr GhcRn -> Bool +isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey +isTagToEnum _ = False + +tcTagToEnum :: HsExpr GhcRn -> HsExpr GhcTc -> [HsExprArg 'TcpTc] + -> TcRhoType -> ExpRhoType + -> TcM (HsExpr GhcTc) +-- tagToEnum# :: forall a. Int# -> a +-- See Note [tagToEnum#] Urgh! +tcTagToEnum expr fun args app_res_ty res_ty + | null val_args + = failWithTc (text "tagToEnum# must appear applied to one argument") + + | otherwise + = do { res_ty <- readExpType res_ty + ; ty' <- zonkTcType res_ty + + -- Check that the type is algebraic + ; case tcSplitTyConApp_maybe ty' of { + Nothing -> do { addErrTc (mk_error ty' doc1) + ; vanilla_result } ; + Just (tc, tc_args) -> + + do { -- Look through any type family + ; fam_envs <- tcGetFamInstEnvs + ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of { + Nothing -> do { check_enumeration ty' tc + ; vanilla_result } ; + Just (rep_tc, rep_args, coi) -> + + do { -- coi :: tc tc_args ~R rep_tc rep_args + check_enumeration ty' rep_tc + ; let rep_ty = mkTyConApp rep_tc rep_args + fun' = mkHsWrap (WpTyApp rep_ty) fun + expr' = rebuildPrefixApps fun' val_args + df_wrap = mkWpCastR (mkTcSymCo coi) + ; return (mkHsWrap df_wrap expr') }}}}} + + where + val_args = dropWhile (not . isHsValArg) args + + vanilla_result + = do { let expr' = rebuildPrefixApps fun args + ; tcWrapResult expr expr' app_res_ty res_ty } + + check_enumeration ty' tc + | isEnumerationTyCon tc = return () + | otherwise = addErrTc (mk_error ty' doc2) + + doc1 = vcat [ text "Specify the type by giving a type signature" + , text "e.g. (tagToEnum# x) :: Bool" ] + doc2 = text "Result type must be an enumeration type" + + mk_error :: TcType -> SDoc -> SDoc + mk_error ty what + = hang (text "Bad call to tagToEnum#" + <+> text "at type" <+> ppr ty) + 2 what + + +{- ********************************************************************* +* * + Pragmas on expressions +* * +********************************************************************* -} + +tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc +tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann + + diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index 1cbdcc005b..82d405f0bb 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -15,10 +15,11 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp - , tcCheckId, tcCheckPolyExpr ) + , tcCheckPolyExpr ) import GHC.Hs import GHC.Tc.Gen.Match +import GHC.Tc.Gen.Head( tcCheckId ) import GHC.Tc.Utils.Zonk( hsLPatType ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 9870c36ff5..9d40225a55 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -14,9 +14,9 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.Tc.Gen.Expr - ( tcCheckPolyExpr, + ( tcCheckPolyExpr, tcCheckPolyExprNC, tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC, - tcInferSigma, tcInferRho, tcInferRhoNC, + tcInferRho, tcInferRhoNC, tcExpr, tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType, tcCheckId, @@ -28,7 +28,6 @@ module GHC.Tc.Gen.Expr import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Gen.Splice( tcSpliceExpr, tcTypedBracket, tcUntypedBracket ) -import GHC.Builtin.Names.TH( liftStringName, liftName ) import GHC.Hs import GHC.Tc.Utils.Zonk @@ -38,18 +37,16 @@ import GHC.Types.Basic import GHC.Core.Multiplicity import GHC.Core.UsageEnv import GHC.Tc.Utils.Instantiate -import GHC.Tc.Gen.Bind ( chooseInferredQuantifiers, tcLocalBinds ) -import GHC.Tc.Gen.Sig ( tcUserTypeSig, tcInstSig ) -import GHC.Tc.Solver ( simplifyInfer, InferMode(..) ) -import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst, tcLookupDataFamInst_maybe ) +import GHC.Tc.Gen.App +import GHC.Tc.Gen.Head +import GHC.Tc.Gen.Bind ( tcLocalBinds ) +import GHC.Tc.Instance.Family ( tcGetFamInstEnvs ) import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Rename.Env ( addUsedGRE ) -import GHC.Rename.Utils ( addNameClashErrRn, unknownSubordinateErr ) import GHC.Tc.Utils.Env import GHC.Tc.Gen.Arrow import GHC.Tc.Gen.Match import GHC.Tc.Gen.HsType -import GHC.Tc.TyCl.PatSyn ( tcPatSynBuilderOcc, nonBidirectionalErr ) import GHC.Tc.Gen.Pat import GHC.Tc.Utils.TcMType import GHC.Tc.Types.Origin @@ -64,19 +61,14 @@ import GHC.Types.Name.Env import GHC.Types.Name.Set import GHC.Types.Name.Reader import GHC.Core.TyCon -import GHC.Core.TyCo.Rep -import GHC.Core.TyCo.Ppr -import GHC.Core.TyCo.Subst (substTyWithInScope) import GHC.Core.Type import GHC.Tc.Types.Evidence import GHC.Types.Var.Set import GHC.Builtin.Types -import GHC.Builtin.PrimOps( tagToEnumKey ) import GHC.Builtin.Names import GHC.Driver.Session import GHC.Types.SrcLoc import GHC.Utils.Misc -import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet ) import GHC.Data.List.SetOps import GHC.Data.Maybe import GHC.Utils.Outputable as Outputable @@ -84,7 +76,7 @@ import GHC.Utils.Panic import GHC.Data.FastString import Control.Monad import GHC.Core.Class(classTyCon) -import GHC.Types.Unique.Set +import GHC.Types.Unique.Set ( UniqSet, mkUniqSet, elementOfUniqSet, nonDetEltsUniqSet ) import qualified GHC.LanguageExtensions as LangExt import Data.Function @@ -118,7 +110,7 @@ tcPolyExpr, tcPolyExprNC -> TcM (LHsExpr GhcTc) tcPolyExpr expr res_ty - = addExprCtxt expr $ + = addLExprCtxt expr $ do { traceTc "tcPolyExpr" (ppr res_ty) ; tcPolyExprNC expr res_ty } @@ -134,21 +126,11 @@ tcPolyExprNC (L loc expr) res_ty set_loc_and_ctxt l e m = do inGenCode <- inGeneratedCode if inGenCode && not (isGeneratedSrcSpan l) - then setSrcSpan l $ addExprCtxt (L l e) m + then setSrcSpan l $ + addExprCtxt e m else setSrcSpan l m --------------- -tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType) --- Used by tcRnExpr to implement GHCi :type --- It goes against the principle of eager instantiation, --- so we expect very very few calls to this function --- Most clients will want tcInferRho -tcInferSigma le@(L loc expr) - = addExprCtxt le $ setSrcSpan loc $ - do { (fun, args, ty) <- tcInferApp expr - ; return (L loc (applyHsArgs fun args), ty) } - ---------------- tcCheckMonoExpr, tcCheckMonoExprNC :: LHsExpr GhcRn -- Expression to type check -> TcRhoType -- Expected type @@ -164,7 +146,7 @@ tcMonoExpr, tcMonoExprNC -> TcM (LHsExpr GhcTc) tcMonoExpr expr res_ty - = addExprCtxt expr $ + = addLExprCtxt expr $ tcMonoExprNC expr res_ty tcMonoExprNC (L loc expr) res_ty @@ -175,7 +157,8 @@ tcMonoExprNC (L loc expr) res_ty --------------- tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. -tcInferRho le = addExprCtxt le (tcInferRhoNC le) +tcInferRho le = addLExprCtxt le $ + tcInferRhoNC le tcInferRhoNC (L loc expr) = setSrcSpan loc $ @@ -189,36 +172,45 @@ tcInferRhoNC (L loc expr) * * ********************************************************************* -} -tcLExpr, tcLExprNC - :: LHsExpr GhcRn -- Expression to type check - -> ExpRhoType -- Expected type - -- Definitely no foralls at the top - -> TcM (LHsExpr GhcTc) - -tcLExpr expr res_ty - = setSrcSpan (getLoc expr) $ addExprCtxt expr (tcLExprNC expr res_ty) - -tcLExprNC (L loc expr) res_ty - = setSrcSpan loc $ - do { expr' <- tcExpr expr res_ty - ; return (L loc expr') } - tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) -tcExpr (HsVar _ (L _ name)) res_ty = tcCheckId name res_ty -tcExpr e@(HsUnboundVar _ uv) res_ty = tcUnboundId e uv res_ty -tcExpr e@(HsApp {}) res_ty = tcApp e res_ty -tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty +-- Use tcApp to typecheck appplications, which are treated specially +-- by Quick Look. Specifically: +-- - HsApp: value applications +-- - HsTypeApp: type applications +-- - HsVar: lone variables, to ensure that they can get an +-- impredicative instantiation (via Quick Look +-- driven by res_ty (in checking mode). +-- - ExprWithTySig: (e :: type) +-- See Note [Application chains and heads] in GHC.Tc.Gen.App +tcExpr e@(HsVar {}) res_ty = tcApp e res_ty +tcExpr e@(HsApp {}) res_ty = tcApp e res_ty +tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty +tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty +tcExpr e@(HsRecFld {}) res_ty = tcApp e res_ty + +-- Typecheck an occurrence of an unbound Id +-- +-- Some of these started life as a true expression hole "_". +-- Others might simply be variables that accidentally have no binding site +tcExpr e@(HsUnboundVar _ occ) res_ty + = do { ty <- newOpenFlexiTyVarTy -- Allow Int# etc (#12531) + ; name <- newSysName occ + ; let ev = mkLocalId name Many ty + ; emitNewExprHole occ ev ty + ; tcWrapResultO (UnboundOccurrenceOf occ) e + (HsUnboundVar ev occ) ty res_ty } tcExpr e@(HsLit x lit) res_ty = do { let lit_ty = hsLitType lit ; tcWrapResult e (HsLit x (convertLit lit)) lit_ty res_ty } -tcExpr (HsPar x expr) res_ty = do { expr' <- tcLExprNC expr res_ty - ; return (HsPar x expr') } +tcExpr (HsPar x expr) res_ty + = do { expr' <- tcMonoExprNC expr res_ty + ; return (HsPar x expr') } tcExpr (HsPragE x prag expr) res_ty - = do { expr' <- tcLExpr expr res_ty + = do { expr' <- tcMonoExpr expr res_ty ; return (HsPragE x (tcExprPrag prag) expr') } tcExpr (HsOverLit x lit) res_ty @@ -229,7 +221,7 @@ tcExpr (NegApp x expr neg_expr) res_ty = do { (expr', neg_expr') <- tcSyntaxOp NegateOrigin neg_expr [SynAny] res_ty $ \[arg_ty] [arg_mult] -> - tcScalingUsage arg_mult $ tcLExpr expr (mkCheckExpType arg_ty) + tcScalingUsage arg_mult $ tcCheckMonoExpr expr arg_ty ; return (NegApp x expr' neg_expr') } tcExpr e@(HsIPVar _ x) res_ty @@ -297,10 +289,6 @@ tcExpr e@(HsLamCase x matches) res_ty , text "requires"] match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody } -tcExpr e@(ExprWithTySig _ expr hs_ty) res_ty - = do { (expr', poly_ty) <- tcExprWithSig expr hs_ty - ; tcWrapResult e expr' poly_ty res_ty } - {- Note [Type-checking overloaded labels] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -345,102 +333,10 @@ With PostfixOperators we don't actually require the function to take two arguments at all. For example, (x `not`) means (not x); you get postfix operators! Not Haskell 98, but it's less work and kind of useful. - -Note [Typing rule for ($)] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -People write - runST $ blah -so much, where - runST :: (forall s. ST s a) -> a -that I have finally given in and written a special type-checking -rule just for saturated applications of ($). - * Infer the type of the first argument - * Decompose it; should be of form (arg2_ty -> res_ty), - where arg2_ty might be a polytype - * Use arg2_ty to typecheck arg2 -} -tcExpr expr@(OpApp fix arg1 op arg2) res_ty - | (L loc (HsVar _ (L lv op_name))) <- op - , op_name `hasKey` dollarIdKey -- Note [Typing rule for ($)] - = do { traceTc "Application rule" (ppr op) - ; (arg1', arg1_ty) <- addErrCtxt (funAppCtxt op arg1 1) $ - tcInferRhoNC arg1 - - ; let doc = text "The first argument of ($) takes" - orig1 = lexprCtOrigin arg1 - ; (wrap_arg1, [arg2_sigma], op_res_ty) <- - matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty - - ; mult_wrap <- tcSubMult AppOrigin Many (scaledMult arg2_sigma) - -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify. - -- - -- When ($) becomes multiplicity-polymorphic, then the above check will - -- need to go. But in the meantime, it would produce ill-typed - -- desugared code to accept linear functions to the left of a ($). - - -- We have (arg1 $ arg2) - -- So: arg1_ty = arg2_ty -> op_res_ty - -- where arg2_sigma maybe polymorphic; that's the point - - ; arg2' <- tcArg nl_op arg2 arg2_sigma 2 - - -- Make sure that the argument type has kind '*' - -- ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b - -- Eg we do not want to allow (D# $ 4.0#) #5570 - -- (which gives a seg fault) - ; _ <- unifyKind (Just (XHsType $ NHsCoreTy (scaledThing arg2_sigma))) - (tcTypeKind (scaledThing arg2_sigma)) liftedTypeKind - -- Ignore the evidence. arg2_sigma must have type * or #, - -- because we know (arg2_sigma -> op_res_ty) is well-kinded - -- (because otherwise matchActualFunTysRho would fail) - -- So this 'unifyKind' will either succeed with Refl, or will - -- produce an insoluble constraint * ~ #, which we'll report later. - - -- NB: unlike the argument type, the *result* type, op_res_ty can - -- have any kind (#8739), so we don't need to check anything for that - - ; op_id <- tcLookupId op_name - ; let op' = L loc (mkHsWrap (mkWpTyApps [ getRuntimeRep op_res_ty - , scaledThing arg2_sigma - , op_res_ty]) - (HsVar noExtField (L lv op_id))) - -- arg1' :: arg1_ty - -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty) - -- op' :: (a2_ty -> op_res_ty) -> a2_ty -> op_res_ty - - expr' = OpApp fix (mkLHsWrap (wrap_arg1 <.> mult_wrap) arg1') op' arg2' - - ; tcWrapResult expr expr' op_res_ty res_ty } - - | L loc (HsRecFld _ (Ambiguous _ lbl)) <- op - , Just sig_ty <- obviousSig (unLoc arg1) - -- See Note [Disambiguating record fields] - = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty - ; sel_name <- disambiguateSelector lbl sig_tc_ty - ; let op' = L loc (HsRecFld noExtField (Unambiguous sel_name lbl)) - ; tcExpr (OpApp fix arg1 op' arg2) res_ty - } - - | otherwise - = do { traceTc "Non Application rule" (ppr op) - ; (op', op_ty) <- tcInferRhoNC op - - ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) - <- matchActualFunTysRho (mk_op_msg op) fn_orig - (Just (unLoc op)) 2 op_ty - -- You might think we should use tcInferApp here, but there is - -- too much impedance-matching, because tcApp may return wrappers as - -- well as type-checked arguments. - - ; arg1' <- tcArg nl_op arg1 arg1_ty 1 - ; arg2' <- tcArg nl_op arg2 arg2_ty 2 - - ; let expr' = OpApp fix arg1' (mkLHsWrap wrap_fun op') arg2' - ; tcWrapResult expr expr' op_res_ty res_ty } - where - fn_orig = exprCtOrigin nl_op - nl_op = unLoc op +tcExpr expr@(OpApp {}) res_ty + = tcApp expr res_ty -- Right sections, equivalent to \ x -> x `op` expr, or -- \ x -> op x expr @@ -449,8 +345,8 @@ tcExpr expr@(SectionR x op arg2) res_ty = do { (op', op_ty) <- tcInferRhoNC op ; (wrap_fun, [Scaled arg1_mult arg1_ty, arg2_ty], op_res_ty) <- matchActualFunTysRho (mk_op_msg op) fn_orig - (Just (unLoc op)) 2 op_ty - ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2 + (Just (ppr op)) 2 op_ty + ; arg2' <- tcValArg (unLoc op) arg2 arg2_ty 2 ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2' act_res_ty = mkVisFunTy arg1_mult arg1_ty op_res_ty ; tcWrapResultMono expr expr' act_res_ty res_ty } @@ -469,8 +365,8 @@ tcExpr expr@(SectionL x arg1 op) res_ty ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty) <- matchActualFunTysRho (mk_op_msg op) fn_orig - (Just (unLoc op)) n_reqd_args op_ty - ; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1 + (Just (ppr op)) n_reqd_args op_ty + ; arg1' <- tcValArg (unLoc op) arg1 arg1_ty 1 ; let expr' = SectionL x arg1' (mkLHsWrap wrap_fn op') act_res_ty = mkVisFunTys arg_tys op_res_ty ; tcWrapResultMono expr expr' act_res_ty res_ty } @@ -510,7 +406,7 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty ; let expr' = ExplicitTuple x tup_args1 boxity missing_tys = [Scaled mult ty | (L _ (Missing (Scaled mult _)), ty) <- zip tup_args1 arg_tys] - -- See Note [Linear fields generalization] + -- See Note [Linear fields generalization] in GHC.Tc.Gen.App act_res_ty = mkVisFunTys missing_tys (mkTupleTy1 boxity arg_tys) -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make @@ -565,7 +461,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty tcExpr (HsLet x (L l binds) expr) res_ty = do { (binds', expr') <- tcLocalBinds binds $ - tcLExpr expr res_ty + tcMonoExpr expr res_ty ; return (HsLet x (L l binds') expr') } tcExpr (HsCase x scrut matches) res_ty @@ -598,9 +494,9 @@ tcExpr (HsCase x scrut matches) res_ty mc_body = tcBody } tcExpr (HsIf x pred b1 b2) res_ty - = do { pred' <- tcLExpr pred (mkCheckExpType boolTy) - ; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty - ; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty + = do { pred' <- tcCheckMonoExpr pred boolTy + ; (u1,b1') <- tcCollectingUsage $ tcMonoExpr b1 res_ty + ; (u2,b2') <- tcCollectingUsage $ tcMonoExpr b2 res_ty ; tcEmitBindingUsage (supUE u1 u2) ; return (HsIf x pred' b1' b2') } @@ -858,7 +754,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty -- -- This should definitely *not* typecheck. - -- STEP -1 See Note [Disambiguating record fields] + -- STEP -1 See Note [Disambiguating record fields] in GHC.Tc.Gen.Head -- After this we know that rbinds is unambiguous ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty ; let upd_flds = map (unLoc . hsRecFieldLbl . unLoc) rbinds @@ -929,7 +825,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty -- Check that we're not dealing with a unidirectional pattern -- synonym ; unless (isJust $ conLikeWrapId_maybe con1) - (nonBidirectionalErr (conLikeName con1)) + (nonBidirectionalErr (conLikeName con1)) -- STEP 3 Note [Criteria for update] -- Check that each updated field is polymorphic; that is, its type @@ -972,7 +868,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty scrut_ty = TcType.substTy scrut_subst con1_res_ty con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys - ; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty + ; co_scrut <- unifyType (Just (ppr record_expr)) record_rho scrut_ty -- NB: normal unification is OK here (as opposed to subsumption), -- because for this to work out, both record_rho and scrut_ty have -- to be normal datatypes -- no contravariant stuff can go on @@ -1012,8 +908,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ; tcWrapResult expr expr' rec_res_ty res_ty } -tcExpr e@(HsRecFld _ f) res_ty - = tcCheckRecSelId e f res_ty {- ************************************************************************ @@ -1069,37 +963,11 @@ tcExpr (XExpr (HsExpanded a b)) t ************************************************************************ -} -tcExpr other _ = pprPanic "tcLExpr" (ppr other) +tcExpr other _ = pprPanic "tcExpr" (ppr other) -- Include ArrForm, ArrApp, which shouldn't appear at all -- Also HsTcBracketOut, HsQuasiQuoteE -{- ********************************************************************* -* * - Pragmas on expressions -* * -********************************************************************* -} - -tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc -tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann - - -{- ********************************************************************* -* * - Expression with type signature e::ty -* * -********************************************************************* -} - -tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn) - -> TcM (HsExpr GhcTc, TcSigmaType) -tcExprWithSig expr hs_ty - = do { sig_info <- checkNoErrs $ -- Avoid error cascade - tcUserTypeSig loc hs_ty Nothing - ; (expr', poly_ty) <- tcExprSig expr sig_info - ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) } - where - loc = getLoc (hsSigWcType hs_ty) - {- ************************************************************************ * * @@ -1160,400 +1028,13 @@ arithSeqEltType (Just fl) res_ty \ [elt_ty] [elt_mult] -> return (elt_mult, elt_ty) ; return (idHsWrapper, elt_mult, elt_ty, Just fl') } -{- -************************************************************************ -* * - Applications -* * -************************************************************************ --} - -{- Note [Typechecking applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We typecheck application chains (f e1 @ty e2) specially: - -* So we can report errors like "in the third arument of a call of f" - -* So we can do Visible Type Application (VTA), for which we must not - eagerly instantiate the function part of the application. - -* So that we can do Quick Look impredicativity. - -The idea is: - -* Use collectHsArgs, which peels off - HsApp, HsTypeApp, HsPrag, HsPar - returning the function in the corner and the arguments - -* Use tcInferAppHead to infer the type of the fuction, - as an (uninstantiated) TcSigmaType - There are special cases for - HsVar, HsREcFld, and ExprWithTySig - Otherwise, delegate back to tcExpr, which - infers an (instantiated) TcRhoType - -Some cases that /won't/ work: - -1. Consider this (which uses visible type application): - - (let { f :: forall a. a -> a; f x = x } in f) @Int - - Since 'let' is not among the special cases for tcInferAppHead, - we'll delegate back to tcExpr, which will instantiate f's type - and the type application to @Int will fail. Too bad! - --} - --- HsExprArg is a very local type, used only within this module. --- It's really a zipper for an application chain --- It's a GHC-specific type, so using TTG only where necessary -data HsExprArg id - = HsEValArg SrcSpan -- Of the function - (LHsExpr (GhcPass id)) - | HsETypeArg SrcSpan -- Of the function - (LHsWcType (NoGhcTc (GhcPass id))) - !(XExprTypeArg id) - | HsEPrag SrcSpan - (HsPragE (GhcPass id)) - | HsEPar SrcSpan -- Of the nested expr - | HsEWrap !(XArgWrap id) -- Wrapper, after typechecking only - --- The outer location is the location of the application itself -type LHsExprArgIn = HsExprArg 'Renamed -type LHsExprArgOut = HsExprArg 'Typechecked - -instance OutputableBndrId id => Outputable (HsExprArg id) where - ppr (HsEValArg _ tm) = ppr tm - ppr (HsEPrag _ p) = text "HsPrag" <+> ppr p - ppr (HsETypeArg _ hs_ty _) = char '@' <> ppr hs_ty - ppr (HsEPar _) = text "HsEPar" - ppr (HsEWrap w) = case ghcPass @id of - GhcTc -> text "HsEWrap" <+> ppr w -#if __GLASGOW_HASKELL__ <= 900 - _ -> empty -#endif - -type family XExprTypeArg id where - XExprTypeArg 'Parsed = NoExtField - XExprTypeArg 'Renamed = NoExtField - XExprTypeArg 'Typechecked = Type - -type family XArgWrap id where - XArgWrap 'Parsed = NoExtCon - XArgWrap 'Renamed = NoExtCon - XArgWrap 'Typechecked = HsWrapper - -addArgWrap :: HsWrapper -> [LHsExprArgOut] -> [LHsExprArgOut] -addArgWrap wrap args - | isIdHsWrapper wrap = args - | otherwise = HsEWrap wrap : args - -collectHsArgs :: HsExpr GhcRn -> (HsExpr GhcRn, [LHsExprArgIn]) -collectHsArgs e = go e [] - where - go (HsPar _ (L l fun)) args = go fun (HsEPar l : args) - go (HsPragE _ p (L l fun)) args = go fun (HsEPrag l p : args) - go (HsApp _ (L l fun) arg) args = go fun (HsEValArg l arg : args) - go (HsAppType _ (L l fun) hs_ty) args = go fun (HsETypeArg l hs_ty noExtField : args) - go e args = (e,args) - -applyHsArgs :: HsExpr GhcTc -> [LHsExprArgOut]-> HsExpr GhcTc -applyHsArgs fun args - = go fun args - where - go fun [] = fun - go fun (HsEWrap wrap : args) = go (mkHsWrap wrap fun) args - go fun (HsEValArg l arg : args) = go (HsApp noExtField (L l fun) arg) args - go fun (HsETypeArg l hs_ty ty : args) = go (HsAppType ty (L l fun) hs_ty) args - go fun (HsEPar l : args) = go (HsPar noExtField (L l fun)) args - go fun (HsEPrag l p : args) = go (HsPragE noExtField p (L l fun)) args - -isHsValArg :: HsExprArg id -> Bool -isHsValArg (HsEValArg {}) = True -isHsValArg _ = False - -isArgPar :: HsExprArg id -> Bool -isArgPar (HsEPar {}) = True -isArgPar _ = False - -getFunLoc :: [HsExprArg 'Renamed] -> Maybe SrcSpan -getFunLoc [] = Nothing -getFunLoc (a:_) = Just $ case a of - HsEValArg l _ -> l - HsETypeArg l _ _ -> l - HsEPrag l _ -> l - HsEPar l -> l - ---------------------------- -tcApp :: HsExpr GhcRn -- either HsApp or HsAppType - -> ExpRhoType -> TcM (HsExpr GhcTc) --- See Note [Typechecking applications] -tcApp expr res_ty - = do { (fun, args, app_res_ty) <- tcInferApp expr - ; if isTagToEnum fun - then tcTagToEnum expr fun args app_res_ty res_ty - -- Done here because we have res_ty, - -- whereas tcInferApp does not - else - - -- The wildly common case - do { let expr' = applyHsArgs fun args - ; addFunResCtxt True fun app_res_ty res_ty $ - tcWrapResult expr expr' app_res_ty res_ty } } - ---------------------------- -tcInferApp :: HsExpr GhcRn - -> TcM ( HsExpr GhcTc -- Function - , [LHsExprArgOut] -- Arguments - , TcSigmaType) -- Inferred type: a sigma-type! --- Also used by Module.tcRnExpr to implement GHCi :type -tcInferApp expr - | -- Gruesome special case for ambiguous record selectors - HsRecFld _ fld_lbl <- fun - , Ambiguous _ lbl <- fld_lbl -- Still ambiguous - , HsEValArg _ (L _ arg) : _ <- filterOut isArgPar args -- A value arg is first - , Just sig_ty <- obviousSig arg -- A type sig on the arg disambiguates - = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty - ; sel_name <- disambiguateSelector lbl sig_tc_ty - ; (tc_fun, fun_ty) <- tcInferRecSelId (Unambiguous sel_name lbl) - ; tcInferApp_finish fun tc_fun fun_ty args } - - | otherwise -- The wildly common case - = do { (tc_fun, fun_ty) <- set_fun_loc (tcInferAppHead fun) - ; tcInferApp_finish fun tc_fun fun_ty args } - where - (fun, args) = collectHsArgs expr - set_fun_loc thing_inside - = case getFunLoc args of - Nothing -> thing_inside -- Don't set the location twice - Just loc -> setSrcSpan loc thing_inside - -tcInferApp_finish - :: HsExpr GhcRn -- Renamed function - -> HsExpr GhcTc -> TcSigmaType -- Function and its type - -> [LHsExprArgIn] -- Arguments - -> TcM (HsExpr GhcTc, [LHsExprArgOut], TcSigmaType) -tcInferApp_finish rn_fun tc_fun fun_sigma rn_args - = do { (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args - ; return (tc_fun, tc_args, actual_res_ty) } - -mk_op_msg :: LHsExpr GhcRn -> SDoc -mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes" - ----------------- -tcInferAppHead :: HsExpr GhcRn -> TcM (HsExpr GhcTc, TcSigmaType) --- Infer type of the head of an application, returning a /SigmaType/ --- i.e. the 'f' in (f e1 ... en) --- We get back a SigmaType because we have special cases for --- * A bare identifier (just look it up) --- This case also covers a record selectro HsRecFld --- * An expression with a type signature (e :: ty) --- --- Note that [] and (,,) are both HsVar: --- see Note [Empty lists] and [ExplicitTuple] in GHC.Hs.Expr --- --- NB: 'e' cannot be HsApp, HsTyApp, HsPrag, HsPar, because those --- cases are dealt with by collectHsArgs. --- --- See Note [Typechecking applications] -tcInferAppHead e - = case e of - HsVar _ (L _ nm) -> tcInferId nm - HsRecFld _ f -> tcInferRecSelId f - ExprWithTySig _ e hs_ty -> add_ctxt $ tcExprWithSig e hs_ty - _ -> add_ctxt $ tcInfer (tcExpr e) - where - add_ctxt thing = addErrCtxt (exprCtxt e) thing - ----------------- --- | Type-check the arguments to a function, possibly including visible type --- applications -tcArgs :: HsExpr GhcRn -- ^ The function itself (for err msgs only) - -> TcSigmaType -- ^ the (uninstantiated) type of the function - -> [LHsExprArgIn] -- ^ the args - -> TcM ([LHsExprArgOut], TcSigmaType) - -- ^ (a wrapper for the function, the tc'd args, result type) -tcArgs fun orig_fun_ty orig_args - = go 1 [] orig_fun_ty orig_args - where - fun_orig = exprCtOrigin fun - herald = sep [ text "The function" <+> quotes (ppr fun) - , text "is applied to"] - - -- Count value args only when complaining about a function - -- applied to too many value args - -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify. - n_val_args = count isHsValArg orig_args - - fun_is_out_of_scope -- See Note [VTA for out-of-scope functions] - = case fun of - HsUnboundVar {} -> True - _ -> False - - go :: Int -- Which argment number this is (incl type args) - -> [Scaled TcSigmaType] -- Value args to which applied so far - -> TcSigmaType - -> [LHsExprArgIn] -> TcM ([LHsExprArgOut], TcSigmaType) - go _ _ fun_ty [] = traceTc "tcArgs:ret" (ppr fun_ty) >> return ([], fun_ty) - - go n so_far fun_ty (HsEPar sp : args) - = do { (args', res_ty) <- go n so_far fun_ty args - ; return (HsEPar sp : args', res_ty) } - - go n so_far fun_ty (HsEPrag sp prag : args) - = do { (args', res_ty) <- go n so_far fun_ty args - ; return (HsEPrag sp (tcExprPrag prag) : args', res_ty) } - - go n so_far fun_ty (HsETypeArg loc hs_ty_arg _ : args) - | fun_is_out_of_scope -- See Note [VTA for out-of-scope functions] - = go (n+1) so_far fun_ty args - - | otherwise - = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty - -- wrap1 :: fun_ty "->" upsilon_ty - ; case tcSplitForAllTy_maybe upsilon_ty of - Just (tvb, inner_ty) - | binderArgFlag tvb == Specified -> - -- It really can't be Inferred, because we've justn - -- instantiated those. But, oddly, it might just be Required. - -- See Note [Required quantifiers in the type of a term] - do { let tv = binderVar tvb - kind = tyVarKind tv - ; ty_arg <- tcHsTypeApp hs_ty_arg kind - - ; inner_ty <- zonkTcType inner_ty - -- See Note [Visible type application zonk] - ; let in_scope = mkInScopeSet (tyCoVarsOfTypes [upsilon_ty, ty_arg]) - insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty - -- NB: tv and ty_arg have the same kind, so this - -- substitution is kind-respecting - ; traceTc "VTA" (vcat [ppr tv, debugPprType kind - , debugPprType ty_arg - , debugPprType (tcTypeKind ty_arg) - , debugPprType inner_ty - , debugPprType insted_ty ]) - - ; (args', res_ty) <- go (n+1) so_far insted_ty args - ; return ( addArgWrap wrap1 $ HsETypeArg loc hs_ty_arg ty_arg : args' - , res_ty ) } - _ -> ty_app_err upsilon_ty hs_ty_arg } - - go n so_far fun_ty (HsEValArg loc arg : args) - = do { (wrap, arg_ty, res_ty) - <- matchActualFunTySigma herald fun_orig (Just fun) - (n_val_args, so_far) fun_ty - ; arg' <- tcArg fun arg arg_ty n - ; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args - ; return ( addArgWrap wrap $ HsEValArg loc arg' : args' - , inner_res_ty ) } - - ty_app_err ty arg - = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty - ; failWith $ - text "Cannot apply expression of type" <+> quotes (ppr ty) $$ - text "to a visible type argument" <+> quotes (ppr arg) } - -{- Note [Required quantifiers in the type of a term] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider (#15859) - - data A k :: k -> Type -- A :: forall k -> k -> Type - type KindOf (a :: k) = k -- KindOf :: forall k. k -> Type - a = (undefind :: KindOf A) @Int - -With ImpredicativeTypes (thin ice, I know), we instantiate -KindOf at type (forall k -> k -> Type), so - KindOf A = forall k -> k -> Type -whose first argument is Required - -We want to reject this type application to Int, but in earlier -GHCs we had an ASSERT that Required could not occur here. - -The ice is thin; c.f. Note [No Required TyCoBinder in terms] -in GHC.Core.TyCo.Rep. - -Note [VTA for out-of-scope functions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose 'wurble' is not in scope, and we have - (wurble @Int @Bool True 'x') - -Then the renamer will make (HsUnboundVar "wurble) for 'wurble', -and the typechecker will typecheck it with tcUnboundId, giving it -a type 'alpha', and emitting a deferred Hole, to be reported later. - -But then comes the visible type application. If we do nothing, we'll -generate an immediate failure (in tc_app_err), saying that a function -of type 'alpha' can't be applied to Bool. That's insane! And indeed -users complain bitterly (#13834, #17150.) - -The right error is the Hole, which has /already/ been emitted by -tcUnboundId. It later reports 'wurble' as out of scope, and tries to -give its type. - -Fortunately in tcArgs we still have access to the function, so we can -check if it is a HsUnboundVar. We use this info to simply skip over -any visible type arguments. We've already inferred the type of the -function, so we'll /already/ have emitted a Hole; -failing preserves that constraint. - -We do /not/ want to fail altogether in this case (via failM) becuase -that may abandon an entire instance decl, which (in the presence of --fdefer-type-errors) leads to leading to #17792. - -Downside; the typechecked term has lost its visible type arguments; we -don't even kind-check them. But let's jump that bridge if we come to -it. Meanwhile, let's not crash! - -Note [Visible type application zonk] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg). - -* tcHsTypeApp only guarantees that - - ty_arg is zonked - - kind(zonk(tv)) = kind(ty_arg) - (checkExpectedKind zonks as it goes). - -So we must zonk inner_ty as well, to guarantee consistency between zonk(tv) -and inner_ty. Otherwise we can build an ill-kinded type. An example was -#14158, where we had: - id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a -and we had the visible type application - id @(->) - -* We instantiated k := kappa, yielding - forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a -* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *). -* That instantiated (->) as ((->) q1 q1), and unified kappa := q1, - Here q1 :: RuntimeRep -* Now we substitute - cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> * - but we must first zonk the inner_ty to get - forall (a :: TYPE q1). cat a a - so that the result of substitution is well-kinded - Failing to do so led to #14158. --} - ----------------- -tcArg :: HsExpr GhcRn -- The function (for error messages) - -> LHsExpr GhcRn -- Actual arguments - -> Scaled TcSigmaType -- expected arg type - -> Int -- # of argument - -> TcM (LHsExpr GhcTc) -- Resulting argument -tcArg fun arg (Scaled mult ty) arg_no - = addErrCtxt (funAppCtxt fun arg arg_no) $ - do { traceTc "tcArg" $ - vcat [ ppr arg_no <+> text "of" <+> ppr fun - , text "arg type:" <+> ppr ty - , text "arg:" <+> ppr arg ] - ; tcScalingUsage mult $ tcCheckPolyExprNC arg ty } - ---------------- tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc] tcTupArgs args tys = ASSERT( equalLength args tys ) mapM go (args `zip` tys) where - go (L l (Missing {}), arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy - ; return (L l (Missing (Scaled mult arg_ty))) } + go (L l (Missing {}), arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy + ; return (L l (Missing (Scaled mult arg_ty))) } go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty ; return (L l (Present x expr')) } @@ -1570,7 +1051,7 @@ tcSyntaxOp :: CtOrigin -> TcM (a, SyntaxExprTc) -- ^ Typecheck a syntax operator -- The operator is a variable or a lambda at this stage (i.e. renamer --- output) +-- output)t tcSyntaxOp orig expr arg_tys res_ty = tcSyntaxOpGen orig expr arg_tys (SynType res_ty) @@ -1583,7 +1064,9 @@ tcSyntaxOpGen :: CtOrigin -> ([TcSigmaType] -> [Mult] -> TcM a) -> TcM (a, SyntaxExprTc) tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside - = do { (expr, sigma) <- tcInferAppHead op + = do { (expr, sigma) <- tcInferAppHead op [] Nothing + -- Nothing here might be improved, but all this + -- code is scheduled for demolition anyway ; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma) ; (result, expr_wrap, arg_wraps, res_wrap) <- tcSynArgA orig sigma arg_tys res_ty $ @@ -1756,497 +1239,14 @@ Here's an example where it actually makes a real difference With the change, f1 will type-check, because the 'Char' info from the signature is propagated into MkQ's argument. With the check in the other order, the extra signature in f2 is reqd. - -************************************************************************ -* * - Expressions with a type signature - expr :: type -* * -********************************************************************* -} - -tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType) -tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc }) - = setSrcSpan loc $ -- Sets the location for the implication constraint - do { let poly_ty = idType poly_id - ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty -> - tcCheckMonoExprNC expr rho_ty - ; return (mkLHsWrap wrap expr', poly_ty) } - -tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) - = setSrcSpan loc $ -- Sets the location for the implication constraint - do { (tclvl, wanted, (expr', sig_inst)) - <- pushLevelAndCaptureConstraints $ - do { sig_inst <- tcInstSig sig - ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $ - tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $ - tcCheckPolyExprNC expr (sig_inst_tau sig_inst) - ; return (expr', sig_inst) } - -- See Note [Partial expression signatures] - ; let tau = sig_inst_tau sig_inst - infer_mode | null (sig_inst_theta sig_inst) - , isNothing (sig_inst_wcx sig_inst) - = ApplyMR - | otherwise - = NoRestrictions - ; (qtvs, givens, ev_binds, residual, _) - <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted - ; emitConstraints residual - - ; tau <- zonkTcType tau - ; let inferred_theta = map evVarPred givens - tau_tvs = tyCoVarsOfType tau - ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta - tau_tvs qtvs (Just sig_inst) - ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau - my_sigma = mkInvisForAllTys binders (mkPhiTy my_theta tau) - ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis. - then return idHsWrapper -- Fast path; also avoids complaint when we infer - -- an ambiguous type and have AllowAmbiguousType - -- e..g infer x :: forall a. F a -> Int - else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma - - ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) - ; let poly_wrap = wrap - <.> mkWpTyLams qtvs - <.> mkWpLams givens - <.> mkWpLet ev_binds - ; return (mkLHsWrap poly_wrap expr', my_sigma) } - - -{- Note [Partial expression signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Partial type signatures on expressions are easy to get wrong. But -here is a guiding principile - e :: ty -should behave like - let x :: ty - x = e - in x - -So for partial signatures we apply the MR if no context is given. So - e :: IO _ apply the MR - e :: _ => IO _ do not apply the MR -just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan - -This makes a difference (#11670): - peek :: Ptr a -> IO CLong - peek ptr = peekElemOff undefined 0 :: _ -from (peekElemOff undefined 0) we get - type: IO w - constraints: Storable w - -We must NOT try to generalise over 'w' because the signature specifies -no constraints so we'll complain about not being able to solve -Storable w. Instead, don't generalise; then _ gets instantiated to -CLong, as it should. -} {- ********************************************************************* * * - tcInferId + Record bindings * * ********************************************************************* -} -tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc) -tcCheckId name res_ty - | name `hasKey` tagToEnumKey - = failWithTc (text "tagToEnum# must appear applied to one argument") - -- tcApp catches the case (tagToEnum# arg) - - | otherwise - = do { (expr, actual_res_ty) <- tcInferId name - ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty]) - ; addFunResCtxt False expr actual_res_ty res_ty $ - tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr - actual_res_ty res_ty } - -tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) -tcCheckRecSelId rn_expr f@(Unambiguous {}) res_ty - = do { (expr, actual_res_ty) <- tcInferRecSelId f - ; tcWrapResult rn_expr expr actual_res_ty res_ty } -tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty - = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of - Nothing -> ambiguousSelector lbl - Just (arg, _) -> do { sel_name <- disambiguateSelector lbl (scaledThing arg) - ; tcCheckRecSelId rn_expr (Unambiguous sel_name lbl) - res_ty } - ------------------------- -tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> TcM (HsExpr GhcTc, TcRhoType) -tcInferRecSelId (Unambiguous sel (L _ lbl)) - = do { (expr', ty) <- tc_infer_id lbl sel - ; return (expr', ty) } -tcInferRecSelId (Ambiguous _ lbl) - = ambiguousSelector lbl - ------------------------- -tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType) --- Look up an occurrence of an Id --- Do not instantiate its type -tcInferId id_name - | id_name `hasKey` assertIdKey - = do { dflags <- getDynFlags - ; if gopt Opt_IgnoreAsserts dflags - then tc_infer_id (nameRdrName id_name) id_name - else tc_infer_assert id_name } - - | otherwise - = do { (expr, ty) <- tc_infer_id (nameRdrName id_name) id_name - ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty) - ; return (expr, ty) } - -tc_infer_assert :: Name -> TcM (HsExpr GhcTc, TcSigmaType) --- Deal with an occurrence of 'assert' --- See Note [Adding the implicit parameter to 'assert'] -tc_infer_assert assert_name - = do { assert_error_id <- tcLookupId assertErrorName - ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name) - (idType assert_error_id) - ; return (mkHsWrap wrap (HsVar noExtField (noLoc assert_error_id)), id_rho) - } - -tc_infer_id :: RdrName -> Name -> TcM (HsExpr GhcTc, TcSigmaType) -tc_infer_id lbl id_name - = do { thing <- tcLookup id_name - ; case thing of - ATcId { tct_id = id } - -> do { check_naughty id -- Note [Local record selectors] - ; checkThLocalId id - ; tcEmitBindingUsage $ unitUE id_name One - ; return_id id } - - AGlobal (AnId id) - -> do { check_naughty id - ; return_id id } - -- A global cannot possibly be ill-staged - -- nor does it need the 'lifting' treatment - -- hence no checkTh stuff here - - AGlobal (AConLike cl) -> case cl of - RealDataCon con -> return_data_con con - PatSynCon ps -> tcPatSynBuilderOcc ps - - _ -> failWithTc $ - ppr thing <+> text "used where a value identifier was expected" } - where - return_id id = return (HsVar noExtField (noLoc id), idType id) - - return_data_con con - = do { let tvs = dataConUserTyVarBinders con - theta = dataConOtherTheta con - args = dataConOrigArgTys con - res = dataConOrigResTy con - - -- See Note [Linear fields generalization] - ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy - ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args' - combine var (Scaled One ty) = Scaled var ty - combine _ scaled_ty = scaled_ty - -- The combine function implements the fact that, as - -- described in Note [Linear fields generalization], if a - -- field is not linear (last line) it isn't made polymorphic. - - etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys - - -- See Note [Instantiating stupid theta] - ; let shouldInstantiate = (not (null (dataConStupidTheta con)) || - isKindLevPoly (tyConResKind (dataConTyCon con))) - ; case shouldInstantiate of - True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs) - ; let tys' = mkTyVarTys tvs' - theta' = substTheta subst theta - args' = substScaledTys subst args - res' = substTy subst res - ; wrap <- instCall (OccurrenceOf id_name) tys' theta' - ; let scaled_arg_tys = scaleArgs args' - eta_wrap = etaWrapper scaled_arg_tys - ; addDataConStupidTheta con tys' - ; return ( mkHsWrap (eta_wrap <.> wrap) - (HsConLikeOut noExtField (RealDataCon con)) - , mkVisFunTys scaled_arg_tys res') - } - False -> let scaled_arg_tys = scaleArgs args - wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs) - eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys) - wrap2 = mkWpTyLams $ binderVars tvs - in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1) - (HsConLikeOut noExtField (RealDataCon con)) - , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res) - } - - check_naughty id - | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl) - | otherwise = return () - - -tcUnboundId :: HsExpr GhcRn -> OccName -> ExpRhoType -> TcM (HsExpr GhcTc) --- Typecheck an occurrence of an unbound Id --- --- Some of these started life as a true expression hole "_". --- Others might simply be variables that accidentally have no binding site --- --- We turn all of them into HsVar, since HsUnboundVar can't contain an --- Id; and indeed the evidence for the ExprHole does bind it, so it's --- not unbound any more! -tcUnboundId rn_expr occ res_ty - = do { ty <- newOpenFlexiTyVarTy -- Allow Int# etc (#12531) - ; name <- newSysName occ - ; let ev = mkLocalId name Many ty - ; emitNewExprHole occ ev ty - ; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr - (HsVar noExtField (noLoc ev)) ty res_ty } - - -{- -Note [Adding the implicit parameter to 'assert'] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The typechecker transforms (assert e1 e2) to (assertError e1 e2). -This isn't really the Right Thing because there's no way to "undo" -if you want to see the original source code in the typechecker -output. We'll have fix this in due course, when we care more about -being able to reconstruct the exact original program. - -Note [tagToEnum#] -~~~~~~~~~~~~~~~~~ -Nasty check to ensure that tagToEnum# is applied to a type that is an -enumeration TyCon. Unification may refine the type later, but this -check won't see that, alas. It's crude, because it relies on our -knowing *now* that the type is ok, which in turn relies on the -eager-unification part of the type checker pushing enough information -here. In theory the Right Thing to do is to have a new form of -constraint but I definitely cannot face that! And it works ok as-is. - -Here's are two cases that should fail - f :: forall a. a - f = tagToEnum# 0 -- Can't do tagToEnum# at a type variable - - g :: Int - g = tagToEnum# 0 -- Int is not an enumeration - -When data type families are involved it's a bit more complicated. - data family F a - data instance F [Int] = A | B | C -Then we want to generate something like - tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int] -Usually that coercion is hidden inside the wrappers for -constructors of F [Int] but here we have to do it explicitly. - -It's all grotesquely complicated. - -Note [Instantiating stupid theta] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Normally, when we infer the type of an Id, we don't instantiate, -because we wish to allow for visible type application later on. -But if a datacon has a stupid theta, we're a bit stuck. We need -to emit the stupid theta constraints with instantiated types. It's -difficult to defer this to the lazy instantiation, because a stupid -theta has no spot to put it in a type. So we just instantiate eagerly -in this case. Thus, users cannot use visible type application with -a data constructor sporting a stupid theta. I won't feel so bad for -the users that complain. - -Note [Linear fields generalization] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As per Note [Polymorphisation of linear fields], linear field of data -constructors get a polymorphic type when the data constructor is used as a term. - - Just :: forall {p} a. a #p-> Maybe a - -This rule is known only to the typechecker: Just keeps its linear type in Core. - -In order to desugar this generalised typing rule, we simply eta-expand: - - \a (x # p :: a) -> Just @a x - -has the appropriate type. We insert these eta-expansion with WpFun wrappers. - -A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums, -certain newtypes with -XUnliftedNewtypes) then this strategy produces - - \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #) - -Which has type - - forall r1 r2 a b. a #p-> b #q-> (# a, b #) - -Which violates the levity-polymorphism restriction see Note [Levity polymorphism -checking] in DsMonad. - -So we really must instantiate r1 and r2 rather than quantify over them. For -simplicity, we just instantiate the entire type, as described in Note -[Instantiating stupid theta]. It breaks visible type application with unboxed -tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used -anywhere. - -A better plan: let's force all representation variable to be *inferred*, so that -they are not subject to visible type applications. Then we can instantiate -inferred argument eagerly. --} - -isTagToEnum :: HsExpr GhcTc -> Bool -isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey -isTagToEnum _ = False - -tcTagToEnum :: HsExpr GhcRn -> HsExpr GhcTc -> [LHsExprArgOut] - -> TcSigmaType -> ExpRhoType - -> TcM (HsExpr GhcTc) --- tagToEnum# :: forall a. Int# -> a --- See Note [tagToEnum#] Urgh! -tcTagToEnum expr fun args app_res_ty res_ty - = do { res_ty <- readExpType res_ty - ; ty' <- zonkTcType res_ty - - -- Check that the type is algebraic - ; case tcSplitTyConApp_maybe ty' of { - Nothing -> do { addErrTc (mk_error ty' doc1) - ; vanilla_result } ; - Just (tc, tc_args) -> - - do { -- Look through any type family - ; fam_envs <- tcGetFamInstEnvs - ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of { - Nothing -> do { check_enumeration ty' tc - ; vanilla_result } ; - Just (rep_tc, rep_args, coi) -> - - do { -- coi :: tc tc_args ~R rep_tc rep_args - check_enumeration ty' rep_tc - ; let val_arg = dropWhile (not . isHsValArg) args - rep_ty = mkTyConApp rep_tc rep_args - fun' = mkHsWrap (WpTyApp rep_ty) fun - expr' = applyHsArgs fun' val_arg - df_wrap = mkWpCastR (mkTcSymCo coi) - ; return (mkHsWrap df_wrap expr') }}}}} - - where - vanilla_result - = do { let expr' = applyHsArgs fun args - ; tcWrapResult expr expr' app_res_ty res_ty } - - check_enumeration ty' tc - | isEnumerationTyCon tc = return () - | otherwise = addErrTc (mk_error ty' doc2) - - doc1 = vcat [ text "Specify the type by giving a type signature" - , text "e.g. (tagToEnum# x) :: Bool" ] - doc2 = text "Result type must be an enumeration type" - - mk_error :: TcType -> SDoc -> SDoc - mk_error ty what - = hang (text "Bad call to tagToEnum#" - <+> text "at type" <+> ppr ty) - 2 what - -{- -************************************************************************ -* * - Template Haskell checks -* * -************************************************************************ --} - -checkThLocalId :: Id -> TcM () --- The renamer has already done checkWellStaged, --- in 'GHC.Rename.Splice.checkThLocalName', so don't repeat that here. --- Here we just add constraints fro cross-stage lifting -checkThLocalId id - = do { mb_local_use <- getStageAndBindLevel (idName id) - ; case mb_local_use of - Just (top_lvl, bind_lvl, use_stage) - | thLevel use_stage > bind_lvl - -> checkCrossStageLifting top_lvl id use_stage - _ -> return () -- Not a locally-bound thing, or - -- no cross-stage link - } - --------------------------------------- -checkCrossStageLifting :: TopLevelFlag -> Id -> ThStage -> TcM () --- If we are inside typed brackets, and (use_lvl > bind_lvl) --- we must check whether there's a cross-stage lift to do --- Examples \x -> [|| x ||] --- [|| map ||] --- --- This is similar to checkCrossStageLifting in GHC.Rename.Splice, but --- this code is applied to *typed* brackets. - -checkCrossStageLifting top_lvl id (Brack _ (TcPending ps_var lie_var q)) - | isTopLevel top_lvl - = when (isExternalName id_name) (keepAlive id_name) - -- See Note [Keeping things alive for Template Haskell] in GHC.Rename.Splice - - | otherwise - = -- Nested identifiers, such as 'x' in - -- E.g. \x -> [|| h x ||] - -- We must behave as if the reference to x was - -- h $(lift x) - -- We use 'x' itself as the splice proxy, used by - -- the desugarer to stitch it all back together. - -- If 'x' occurs many times we may get many identical - -- bindings of the same splice proxy, but that doesn't - -- matter, although it's a mite untidy. - do { let id_ty = idType id - ; checkTc (isTauTy id_ty) (polySpliceErr id) - -- If x is polymorphic, its occurrence sites might - -- have different instantiations, so we can't use plain - -- 'x' as the splice proxy name. I don't know how to - -- solve this, and it's probably unimportant, so I'm - -- just going to flag an error for now - - ; lift <- if isStringTy id_ty then - do { sid <- tcLookupId GHC.Builtin.Names.TH.liftStringName - -- See Note [Lifting strings] - ; return (HsVar noExtField (noLoc sid)) } - else - setConstraintVar lie_var $ - -- Put the 'lift' constraint into the right LIE - newMethodFromName (OccurrenceOf id_name) - GHC.Builtin.Names.TH.liftName - [getRuntimeRep id_ty, id_ty] - - -- Update the pending splices - ; ps <- readMutVar ps_var - ; let pending_splice = PendingTcSplice id_name - (nlHsApp (mkLHsWrap (applyQuoteWrapper q) (noLoc lift)) - (nlHsVar id)) - ; writeMutVar ps_var (pending_splice : ps) - - ; return () } - where - id_name = idName id - -checkCrossStageLifting _ _ _ = return () - -polySpliceErr :: Id -> SDoc -polySpliceErr id - = text "Can't splice the polymorphic local variable" <+> quotes (ppr id) - -{- -Note [Lifting strings] -~~~~~~~~~~~~~~~~~~~~~~ -If we see $(... [| s |] ...) where s::String, we don't want to -generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc. -So this conditional short-circuits the lifting mechanism to generate -(liftString "xy") in that case. I didn't want to use overlapping instances -for the Lift class in TH.Syntax, because that can lead to overlapping-instance -errors in a polymorphic situation. - -If this check fails (which isn't impossible) we get another chance; see -Note [Converting strings] in "GHC.ThToHs" - -Local record selectors -~~~~~~~~~~~~~~~~~~~~~~ -Record selectors for TyCons in this module are ordinary local bindings, -which show up as ATcIds rather than AGlobals. So we need to check for -naughtiness in both branches. c.f. TcTyClsBindings.mkAuxBinds. - - -************************************************************************ -* * -\subsection{Record bindings} -* * -************************************************************************ --} - getFixedTyVars :: [FieldLabelString] -> [TyVar] -> [ConLike] -> TyVarSet -- These tyvars must not change across the updates getFixedTyVars upd_fld_occs univ_tvs cons @@ -2271,129 +1271,9 @@ getFixedTyVars upd_fld_occs univ_tvs cons , (tv1,tv) <- univ_tvs `zip` u_tvs , tv `elemVarSet` fixed_tvs ] -{- -Note [Disambiguating record fields] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When the -XDuplicateRecordFields extension is used, and the renamer -encounters a record selector or update that it cannot immediately -disambiguate (because it involves fields that belong to multiple -datatypes), it will defer resolution of the ambiguity to the -typechecker. In this case, the `Ambiguous` constructor of -`AmbiguousFieldOcc` is used. - -Consider the following definitions: - - data S = MkS { foo :: Int } - data T = MkT { foo :: Int, bar :: Int } - data U = MkU { bar :: Int, baz :: Int } - -When the renamer sees `foo` as a selector or an update, it will not -know which parent datatype is in use. - -For selectors, there are two possible ways to disambiguate: - -1. Check if the pushed-in type is a function whose domain is a - datatype, for example: - - f s = (foo :: S -> Int) s - - g :: T -> Int - g = foo - - This is checked by `tcCheckRecSelId` when checking `HsRecFld foo`. - -2. Check if the selector is applied to an argument that has a type - signature, for example: - - h = foo (s :: S) - - This is checked by `tcApp`. - - -Updates are slightly more complex. The `disambiguateRecordBinds` -function tries to determine the parent datatype in three ways: - -1. Check for types that have all the fields being updated. For example: - - f x = x { foo = 3, bar = 2 } - - Here `f` must be updating `T` because neither `S` nor `U` have - both fields. This may also discover that no possible type exists. - For example the following will be rejected: - - f' x = x { foo = 3, baz = 3 } - -2. Use the type being pushed in, if it is already a TyConApp. The - following are valid updates to `T`: - - g :: T -> T - g x = x { foo = 3 } - - g' x = x { foo = 3 } :: T - -3. Use the type signature of the record expression, if it exists and - is a TyConApp. Thus this is valid update to `T`: - - h x = (x :: T) { foo = 3 } - - -Note that we do not look up the types of variables being updated, and -no constraint-solving is performed, so for example the following will -be rejected as ambiguous: - - let bad (s :: S) = foo s - - let r :: T - r = blah - in r { foo = 3 } - - \r. (r { foo = 3 }, r :: T ) - -We could add further tests, of a more heuristic nature. For example, -rather than looking for an explicit signature, we could try to infer -the type of the argument to a selector or the record expression being -updated, in case we are lucky enough to get a TyConApp straight -away. However, it might be hard for programmers to predict whether a -particular update is sufficiently obvious for the signature to be -omitted. Moreover, this might change the behaviour of typechecker in -non-obvious ways. - -See also Note [HsRecField and HsRecUpdField] in GHC.Hs.Pat. --} - --- Given a RdrName that refers to multiple record fields, and the type --- of its argument, try to determine the name of the selector that is --- meant. -disambiguateSelector :: Located RdrName -> Type -> TcM Name -disambiguateSelector lr@(L _ rdr) parent_type - = do { fam_inst_envs <- tcGetFamInstEnvs - ; case tyConOf fam_inst_envs parent_type of - Nothing -> ambiguousSelector lr - Just p -> - do { xs <- lookupParents rdr - ; let parent = RecSelData p - ; case lookup parent xs of - Just gre -> do { addUsedGRE True gre - ; return (gre_name gre) } - Nothing -> failWithTc (fieldNotInType parent rdr) } } - --- This field name really is ambiguous, so add a suitable "ambiguous --- occurrence" error, then give up. -ambiguousSelector :: Located RdrName -> TcM a -ambiguousSelector (L _ rdr) - = do { addAmbiguousNameErr rdr - ; failM } - --- | This name really is ambiguous, so add a suitable "ambiguous --- occurrence" error, then continue -addAmbiguousNameErr :: RdrName -> TcM () -addAmbiguousNameErr rdr - = do { env <- getGlobalRdrEnv - ; let gres = lookupGRE_RdrName rdr env - ; setErrCtxt [] $ addNameClashErrRn rdr gres} -- Disambiguate the fields in a record update. --- See Note [Disambiguating record fields] +-- See Note [Disambiguating record fields] in GHC.Tc.Gen.Head disambiguateRecordBinds :: LHsExpr GhcRn -> TcRhoType -> [LHsRecUpdField GhcRn] -> ExpRhoType -> TcM [LHsRecField' (AmbiguousFieldOcc GhcTc) (LHsExpr GhcRn)] @@ -2488,44 +1368,6 @@ disambiguateRecordBinds record_expr record_rho rbnds res_ty = L loc (Unambiguous i (L loc lbl)) } } --- Extract the outermost TyCon of a type, if there is one; for --- data families this is the representation tycon (because that's --- where the fields live). -tyConOf :: FamInstEnvs -> TcSigmaType -> Maybe TyCon -tyConOf fam_inst_envs ty0 - = case tcSplitTyConApp_maybe ty of - Just (tc, tys) -> Just (fstOf3 (tcLookupDataFamInst fam_inst_envs tc tys)) - Nothing -> Nothing - where - (_, _, ty) = tcSplitSigmaTy ty0 - --- Variant of tyConOf that works for ExpTypes -tyConOfET :: FamInstEnvs -> ExpRhoType -> Maybe TyCon -tyConOfET fam_inst_envs ty0 = tyConOf fam_inst_envs =<< checkingExpType_maybe ty0 - --- For an ambiguous record field, find all the candidate record --- selectors (as GlobalRdrElts) and their parents. -lookupParents :: RdrName -> RnM [(RecSelParent, GlobalRdrElt)] -lookupParents rdr - = do { env <- getGlobalRdrEnv - ; let gres = lookupGRE_RdrName rdr env - ; mapM lookupParent gres } - where - lookupParent :: GlobalRdrElt -> RnM (RecSelParent, GlobalRdrElt) - lookupParent gre = do { id <- tcLookupId (gre_name gre) - ; if isRecordSelector id - then return (recordSelectorTyCon id, gre) - else failWithTc (notSelector (gre_name gre)) } - --- A type signature on the argument of an ambiguous record selector or --- the record expression in an update must be "obvious", i.e. the --- outermost constructor ignoring parentheses. -obviousSig :: HsExpr GhcRn -> Maybe (LHsSigWcType GhcRn) -obviousSig (ExprWithTySig _ _ ty) = Just ty -obviousSig (HsPar _ p) = obviousSig (unLoc p) -obviousSig _ = Nothing - - {- Game plan for record bindings ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2538,7 +1380,7 @@ For each binding field = value 3. Instantiate the field type (from the field label) using the type envt from step 2. -4 Type check the value using tcArg, passing the field type as +4 Type check the value using tcValArg, passing the field type as the expected argument type. This extends OK when the field types are universally quantified. @@ -2678,103 +1520,8 @@ fieldCtxt :: FieldLabelString -> SDoc fieldCtxt field_name = text "In the" <+> quotes (ppr field_name) <+> ptext (sLit "field of a record") -addExprCtxt :: LHsExpr GhcRn -> TcRn a -> TcRn a -addExprCtxt e thing_inside = addErrCtxt (exprCtxt (unLoc e)) thing_inside - -exprCtxt :: HsExpr GhcRn -> SDoc -exprCtxt expr = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr)) - -addFunResCtxt :: Bool -- There is at least one argument - -> HsExpr GhcTc -> TcType -> ExpRhoType - -> TcM a -> TcM a --- When we have a mis-match in the return type of a function --- try to give a helpful message about too many/few arguments --- --- Used for naked variables too; but with has_args = False -addFunResCtxt has_args fun fun_res_ty env_ty - = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg) - -- NB: use a landmark error context, so that an empty context - -- doesn't suppress some more useful context - where - mk_msg - = do { mb_env_ty <- readExpType_maybe env_ty - -- by the time the message is rendered, the ExpType - -- will be filled in (except if we're debugging) - ; fun_res' <- zonkTcType fun_res_ty - ; env' <- case mb_env_ty of - Just env_ty -> zonkTcType env_ty - Nothing -> - do { dumping <- doptM Opt_D_dump_tc_trace - ; MASSERT( dumping ) - ; newFlexiTyVarTy liftedTypeKind } - ; let -- See Note [Splitting nested sigma types in mismatched - -- function types] - (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res' - -- No need to call tcSplitNestedSigmaTys here, since env_ty is - -- an ExpRhoTy, i.e., it's already instantiated. - (_, _, env_tau) = tcSplitSigmaTy env' - (args_fun, res_fun) = tcSplitFunTys fun_tau - (args_env, res_env) = tcSplitFunTys env_tau - n_fun = length args_fun - n_env = length args_env - info | n_fun == n_env = Outputable.empty - | n_fun > n_env - , not_fun res_env - = text "Probable cause:" <+> quotes (ppr fun) - <+> text "is applied to too few arguments" - - | has_args - , not_fun res_fun - = text "Possible cause:" <+> quotes (ppr fun) - <+> text "is applied to too many arguments" - - | otherwise - = Outputable.empty -- Never suggest that a naked variable is -- applied to too many args! - ; return info } - where - not_fun ty -- ty is definitely not an arrow type, - -- and cannot conceivably become one - = case tcSplitTyConApp_maybe ty of - Just (tc, _) -> isAlgTyCon tc - Nothing -> False - -{- -Note [Splitting nested sigma types in mismatched function types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When one applies a function to too few arguments, GHC tries to determine this -fact if possible so that it may give a helpful error message. It accomplishes -this by checking if the type of the applied function has more argument types -than supplied arguments. - -Previously, GHC computed the number of argument types through tcSplitSigmaTy. -This is incorrect in the face of nested foralls, however! This caused Trac -#13311, for instance: - - f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b - -If one uses `f` like so: - - do { f; putChar 'a' } - -Then tcSplitSigmaTy will decompose the type of `f` into: - - Tyvars: [a] - Context: (Monoid a) - Argument types: [] - Return type: forall b. Monoid b => Maybe a -> Maybe b - -That is, it will conclude that there are *no* argument types, and since `f` -was given no arguments, it won't print a helpful error message. On the other -hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to: - - Tyvars: [a, b] - Context: (Monoid a, Monoid b) - Argument types: [Maybe a] - Return type: Maybe b - -So now GHC recognizes that `f` has one more argument type than it was actually -provided. --} +mk_op_msg :: LHsExpr GhcRn -> SDoc +mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes" badFieldTypes :: [(FieldLabelString,TcType)] -> SDoc badFieldTypes prs @@ -2818,7 +1565,7 @@ badFieldsUpd rbinds data_cons -- For each field, which constructors contain the field? membership :: [(FieldLabelString, [Bool])] membership = sortMembership $ - map (\fld -> (fld, map (elementOfUniqSet fld) fieldLabelSets)) $ + map (\fld -> (fld, map (fld `elementOfUniqSet`) fieldLabelSets)) $ map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc . unLoc . hsRecFieldLbl . unLoc) rbinds fieldLabelSets :: [UniqSet FieldLabelString] @@ -2858,16 +1605,6 @@ Finding the smallest subset is hard, so the code here makes a decent stab, no more. See #7989. -} -naughtyRecordSel :: RdrName -> SDoc -naughtyRecordSel sel_id - = text "Cannot use record selector" <+> quotes (ppr sel_id) <+> - text "as a function due to escaped type variables" $$ - text "Probable fix: use pattern-matching syntax instead" - -notSelector :: Name -> SDoc -notSelector field - = hsep [quotes (ppr field), text "is not a record selector"] - mixedSelectors :: [Id] -> [Id] -> SDoc mixedSelectors data_sels@(dc_rep_id:_) pat_syn_sels@(ps_rep_id:_) = ptext @@ -2918,10 +1655,6 @@ noPossibleParents rbinds badOverloadedUpdate :: SDoc badOverloadedUpdate = text "Record update is ambiguous, and requires a type signature" -fieldNotInType :: RecSelParent -> RdrName -> SDoc -fieldNotInType p rdr - = unknownSubordinateErr (text "field of type" <+> quotes (ppr p)) rdr - {- ************************************************************************ * * diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot index 0676799b11..0a04b6d9e9 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs-boot +++ b/compiler/GHC/Tc/Gen/Expr.hs-boot @@ -1,13 +1,13 @@ module GHC.Tc.Gen.Expr where -import GHC.Types.Name -import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn, SyntaxExprTc ) +import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn + , SyntaxExprTc ) import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Origin ( CtOrigin ) import GHC.Core.Type ( Mult ) import GHC.Hs.Extension ( GhcRn, GhcTc ) -tcCheckPolyExpr :: +tcCheckPolyExpr, tcCheckPolyExprNC :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTc) @@ -23,8 +23,6 @@ tcCheckMonoExpr, tcCheckMonoExprNC :: tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) -tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType) - tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) @@ -42,5 +40,3 @@ tcSyntaxOpGen :: CtOrigin -> ([TcSigmaType] -> [Mult] -> TcM a) -> TcM (a, SyntaxExprTc) - -tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc) diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs new file mode 100644 index 0000000000..530f985a95 --- /dev/null +++ b/compiler/GHC/Tc/Gen/Head.hs @@ -0,0 +1,1143 @@ +{- +% +(c) The University of Glasgow 2006 +(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 +-} + +{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeApplications #-} +{-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow] + +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} + +module GHC.Tc.Gen.Head + ( HsExprArg(..), EValArg(..), TcPass(..), Rebuilder + , splitHsApps + , addArgWrap, eValArgExpr, isHsValArg, setSrcSpanFromArgs + , countLeadingValArgs, isVisibleArg, pprHsExprArgTc, rebuildPrefixApps + + , tcInferAppHead, tcInferAppHead_maybe + , tcInferId, tcCheckId + , obviousSig, addAmbiguousNameErr + , tyConOf, tyConOfET, lookupParents, fieldNotInType + , notSelector, nonBidirectionalErr + + , addExprCtxt, addLExprCtxt, addFunResCtxt ) where + +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC ) + +import GHC.Tc.Gen.HsType +import GHC.Tc.Gen.Pat +import GHC.Tc.Gen.Bind( chooseInferredQuantifiers ) +import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig ) +import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc ) +import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.Unify +import GHC.Types.Basic +import GHC.Tc.Utils.Instantiate +import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst ) +import GHC.Core.FamInstEnv ( FamInstEnvs ) +import GHC.Core.UsageEnv ( unitUE ) +import GHC.Rename.Env ( addUsedGRE ) +import GHC.Rename.Utils ( addNameClashErrRn, unknownSubordinateErr ) +import GHC.Tc.Solver ( InferMode(..), simplifyInfer ) +import GHC.Tc.Utils.Env +import GHC.Tc.Utils.TcMType +import GHC.Tc.Types.Origin +import GHC.Tc.Utils.TcType as TcType +import GHC.Hs +import GHC.Types.Id +import GHC.Types.Id.Info +import GHC.Core.ConLike +import GHC.Core.DataCon +import GHC.Types.Name +import GHC.Types.Name.Reader +import GHC.Core.TyCon +import GHC.Core.TyCo.Rep +import GHC.Core.Type +import GHC.Tc.Types.Evidence +import GHC.Builtin.Types( multiplicityTy ) +import GHC.Builtin.Names +import GHC.Builtin.Names.TH( liftStringName, liftName ) +import GHC.Driver.Session +import GHC.Types.SrcLoc +import GHC.Utils.Misc +import GHC.Data.Maybe +import GHC.Utils.Outputable as Outputable +import GHC.Utils.Panic +import Control.Monad + +import Data.Function + +#include "HsVersions.h" + +import GHC.Prelude + + +{- ********************************************************************* +* * + HsExprArg: auxiliary data type +* * +********************************************************************* -} + +{- Note [HsExprArg] +~~~~~~~~~~~~~~~~~~~ +The data type HsExprArg :: TcPass -> Type +is a very local type, used only within this module and GHC.Tc.Gen.App + +* It's really a zipper for an application chain + See Note [Application chains and heads] in GHC.Tc.Gen.App for + what an "application chain" is. + +* It's a GHC-specific type, so using TTG only where necessary + +* It is indexed by TcPass, meaning + - HsExprArg TcpRn: + The result of splitHsApps, which decomposes a HsExpr GhcRn + + - HsExprArg TcpInst: + The result of tcInstFun, which instantiates the function type + Adds EWrap nodes, the argument type in EValArg, + and the kind-checked type in ETypeArg + + - HsExprArg TcpTc: + The result of tcArg, which typechecks the value args + In EValArg we now have a (LHsExpr GhcTc) + +* rebuildPrefixApps is dual to splitHsApps, and zips an application + back into a HsExpr + +Note [EValArg] +~~~~~~~~~~~~~~ +The data type EValArg is the payload of the EValArg constructor of +HsExprArg; i.e. a value argument of the application. EValArg has two +forms: + +* ValArg: payload is just the expression itself. Simple. + +* ValArgQL: captures the results of applying quickLookArg to the + argument in a ValArg. When we later want to typecheck that argument + we can just carry on from where quick-look left off. The fields of + ValArgQL exactly capture what is needed to complete the job. + +Invariants: + +1. With QL switched off, all arguments are ValArg; no ValArgQL + +2. With QL switched on, tcInstFun converts some ValArgs to ValArgQL, + under the conditions when quick-look should happen (eg the argument + type is guarded) -- see quickLookArg + +Note [splitHsApps and Rebuilder] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The key function + splitHsApps :: HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder) +takes apart either an HsApp, or an infix OpApp, returning + +* The "head" of the application, an expression that is often a variable + +* A list of HsExprArg, the arguments + +* A Rebuilder function which reconstructs the original form, given the + head and arguments. This allows us to reconstruct infix + applications (OpApp) as well as prefix applications (HsApp), + thereby retaining the structure of the original tree. +-} + +data TcPass = TcpRn -- Arguments decomposed + | TcpInst -- Function instantiated + | TcpTc -- Typechecked + +data HsExprArg (p :: TcPass) + = -- See Note [HsExprArg] + EValArg { eva_loc :: SrcSpan -- Of the function + , eva_arg :: EValArg p + , eva_arg_ty :: !(XEVAType p) } + + | ETypeArg { eva_loc :: SrcSpan -- Of the function + , eva_hs_ty :: LHsWcType GhcRn -- The type arg + , eva_ty :: !(XETAType p) } -- Kind-checked type arg + + | EPrag SrcSpan + (HsPragE (GhcPass (XPass p))) + + | EPar SrcSpan -- Of the nested expr + + | EWrap !(XEWrap p) -- Wrapper, after instantiation + +data EValArg (p :: TcPass) where -- See Note [EValArg] + ValArg :: LHsExpr (GhcPass (XPass p)) + -> EValArg p + ValArgQL :: { va_expr :: LHsExpr GhcRn -- Original expression + -- For location and error msgs + , va_fun :: HsExpr GhcTc -- Function, typechecked + , va_args :: [HsExprArg 'TcpInst] -- Args, instantiated + , va_ty :: TcRhoType -- Result type + , va_rebuild :: Rebuilder } -- How to reassemble + -> EValArg 'TcpInst -- Only exists in TcpInst phase + +type Rebuilder = HsExpr GhcTc -> [HsExprArg 'TcpTc]-> HsExpr GhcTc +-- See Note [splitHsApps and Rebuilder] + +type family XPass p where + XPass 'TcpRn = 'Renamed + XPass 'TcpInst = 'Renamed + XPass 'TcpTc = 'Typechecked + +type family XETAType p where -- Type arguments + XETAType 'TcpRn = NoExtField + XETAType _ = Type + +type family XEVAType p where -- Value arguments + XEVAType 'TcpRn = NoExtField + XEVAType _ = Scaled Type + +type family XEWrap p where + XEWrap 'TcpRn = NoExtCon + XEWrap _ = HsWrapper + +mkEValArg :: SrcSpan -> LHsExpr GhcRn -> HsExprArg 'TcpRn +mkEValArg l e = EValArg { eva_loc = l, eva_arg = ValArg e + , eva_arg_ty = noExtField } + +mkETypeArg :: SrcSpan -> LHsWcType GhcRn -> HsExprArg 'TcpRn +mkETypeArg l hs_ty = ETypeArg { eva_loc = l, eva_hs_ty = hs_ty + , eva_ty = noExtField } + +eValArgExpr :: EValArg 'TcpInst -> LHsExpr GhcRn +eValArgExpr (ValArg e) = e +eValArgExpr (ValArgQL { va_expr = e }) = e + +addArgWrap :: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst] +addArgWrap wrap args + | isIdHsWrapper wrap = args + | otherwise = EWrap wrap : args + +splitHsApps :: HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder) +-- See Note [splitHsApps and Rebuilder] +splitHsApps e + = go e [] + where + go (HsPar _ (L l fun)) args = go fun (EPar l : args) + go (HsPragE _ p (L l fun)) args = go fun (EPrag l p : args) + go (HsAppType _ (L l fun) hs_ty) args = go fun (mkETypeArg l hs_ty : args) + go (HsApp _ (L l fun) arg) args = go fun (mkEValArg l arg : args) + + go (OpApp fix arg1 (L l op) arg2) args + = (op, mkEValArg l arg1 : mkEValArg l arg2 : args, rebuild_infix fix) + + go e args = (e, args, rebuildPrefixApps) + + rebuild_infix :: Fixity -> Rebuilder + rebuild_infix fix fun args + = go fun args + where + go fun (EValArg { eva_arg = ValArg arg1, eva_loc = l } : + EValArg { eva_arg = ValArg arg2 } : args) + = rebuildPrefixApps (OpApp fix arg1 (L l fun) arg2) args + go fun (EWrap wrap : args) = go (mkHsWrap wrap fun) args + go fun args = rebuildPrefixApps fun args + -- This last case fails to rebuild a OpApp, which is sad. + -- It can happen if we have (e1 `op` e2), + -- and op :: Int -> forall a. a -> Int, and e2 :: Bool + -- Then we'll get [ e1, @Bool, e2 ] + -- Could be fixed with WpFun, but extra complexity. + +rebuildPrefixApps :: Rebuilder +rebuildPrefixApps fun args + = go fun args + where + go fun [] = fun + go fun (EWrap wrap : args) = go (mkHsWrap wrap fun) args + go fun (EValArg { eva_arg = ValArg arg + , eva_loc = l } : args) = go (HsApp noExtField (L l fun) arg) args + go fun (ETypeArg { eva_hs_ty = hs_ty + , eva_ty = ty + , eva_loc = l } : args) = go (HsAppType ty (L l fun) hs_ty) args + go fun (EPar l : args) = go (HsPar noExtField (L l fun)) args + go fun (EPrag l p : args) = go (HsPragE noExtField p (L l fun)) args + +isHsValArg :: HsExprArg id -> Bool +isHsValArg (EValArg {}) = True +isHsValArg _ = False + +countLeadingValArgs :: [HsExprArg id] -> Int +countLeadingValArgs (EValArg {} : args) = 1 + countLeadingValArgs args +countLeadingValArgs (EPar {} : args) = countLeadingValArgs args +countLeadingValArgs (EPrag {} : args) = countLeadingValArgs args +countLeadingValArgs _ = 0 + +isValArg :: HsExprArg id -> Bool +isValArg (EValArg {}) = True +isValArg _ = False + +isVisibleArg :: HsExprArg id -> Bool +isVisibleArg (EValArg {}) = True +isVisibleArg (ETypeArg {}) = True +isVisibleArg _ = False + +setSrcSpanFromArgs :: [HsExprArg 'TcpRn] -> TcM a -> TcM a +setSrcSpanFromArgs [] thing_inside + = thing_inside +setSrcSpanFromArgs (arg:_) thing_inside + = setSrcSpan (argFunLoc arg) thing_inside + +argFunLoc :: HsExprArg 'TcpRn -> SrcSpan +argFunLoc (EValArg { eva_loc = l }) = l +argFunLoc (ETypeArg { eva_loc = l}) = l +argFunLoc (EPrag l _) = l +argFunLoc (EPar l) = l + +instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where + ppr (EValArg { eva_arg = arg }) = text "EValArg" <+> ppr arg + ppr (EPrag _ p) = text "EPrag" <+> ppr p + ppr (ETypeArg { eva_hs_ty = hs_ty }) = char '@' <> ppr hs_ty + ppr (EPar _) = text "EPar" + ppr (EWrap _) = text "EWrap" + -- ToDo: to print the wrapper properly we'll need to work harder + -- "Work harder" = replicate the ghcPass approach, but I didn't + -- think it was worth the effort to do so. + +instance OutputableBndrId (XPass p) => Outputable (EValArg p) where + ppr (ValArg e) = ppr e + ppr (ValArgQL { va_fun = fun, va_args = args, va_ty = ty}) + = hang (text "ValArgQL" <+> ppr fun) + 2 (vcat [ ppr args, text "va_ty:" <+> ppr ty ]) + +pprHsExprArgTc :: HsExprArg 'TcpInst -> SDoc +pprHsExprArgTc (EValArg { eva_arg = tm, eva_arg_ty = ty }) + = text "EValArg" <+> hang (ppr tm) 2 (dcolon <+> ppr ty) +pprHsExprArgTc arg = ppr arg + + +{- ********************************************************************* +* * + tcInferAppHead +* * +********************************************************************* -} + +tcInferAppHead :: HsExpr GhcRn + -> [HsExprArg 'TcpRn] -> Maybe TcRhoType + -- These two args are solely for tcInferRecSelId + -> TcM (HsExpr GhcTc, TcSigmaType) +-- Infer type of the head of an application +-- i.e. the 'f' in (f e1 ... en) +-- See Note [Application chains and heads] in GHC.Tc.Gen.App +-- We get back a /SigmaType/ because we have special cases for +-- * A bare identifier (just look it up) +-- This case also covers a record selectro HsRecFld +-- * An expression with a type signature (e :: ty) +-- See Note [Application chains and heads] in GHC.Tc.Gen.App +-- +-- Why do we need the arguments to infer the type of the head of +-- the application? For two reasons: +-- * (Legitimate) The first arg has the source location of the head +-- * (Disgusting) Needed for record disambiguation; see tcInferRecSelId +-- +-- Note that [] and (,,) are both HsVar: +-- see Note [Empty lists] and [ExplicitTuple] in GHC.Hs.Expr +-- +-- NB: 'e' cannot be HsApp, HsTyApp, HsPrag, HsPar, because those +-- cases are dealt with by splitHsApps. +-- +-- See Note [tcApp: typechecking applications] in GHC.Tc.Gen.App +tcInferAppHead fun args mb_res_ty + = setSrcSpanFromArgs args $ + do { mb_tc_fun <- tcInferAppHead_maybe fun args mb_res_ty + ; case mb_tc_fun of + Just (fun', fun_sigma) -> return (fun', fun_sigma) + Nothing -> add_head_ctxt fun args $ + tcInfer (tcExpr fun) } + +tcInferAppHead_maybe :: HsExpr GhcRn + -> [HsExprArg 'TcpRn] -> Maybe TcRhoType + -- These two args are solely for tcInferRecSelId + -> TcM (Maybe (HsExpr GhcTc, TcSigmaType)) +-- See Note [Application chains and heads] in GHC.Tc.Gen.App +-- Returns Nothing for a complicated head +tcInferAppHead_maybe fun args mb_res_ty + = case fun of + HsVar _ (L _ nm) -> Just <$> tcInferId nm + HsRecFld _ f -> Just <$> tcInferRecSelId f args mb_res_ty + ExprWithTySig _ e hs_ty -> add_head_ctxt fun args $ + Just <$> tcExprWithSig e hs_ty + _ -> return Nothing + +add_head_ctxt :: HsExpr GhcRn -> [HsExprArg 'TcpRn] -> TcM a -> TcM a +-- Don't push an expression context if the arguments are empty, +-- because it has already been pushed by tcExpr +add_head_ctxt fun args thing_inside + | null args = thing_inside + | otherwise = addExprCtxt fun thing_inside + + +{- ********************************************************************* +* * + Record selectors +* * +********************************************************************* -} + +{- Note [Disambiguating record fields] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When the -XDuplicateRecordFields extension is used, and the renamer +encounters a record selector or update that it cannot immediately +disambiguate (because it involves fields that belong to multiple +datatypes), it will defer resolution of the ambiguity to the +typechecker. In this case, the `Ambiguous` constructor of +`AmbiguousFieldOcc` is used. + +Consider the following definitions: + + data S = MkS { foo :: Int } + data T = MkT { foo :: Int, bar :: Int } + data U = MkU { bar :: Int, baz :: Int } + +When the renamer sees `foo` as a selector or an update, it will not +know which parent datatype is in use. + +For selectors, there are two possible ways to disambiguate: + +1. Check if the pushed-in type is a function whose domain is a + datatype, for example: + + f s = (foo :: S -> Int) s + + g :: T -> Int + g = foo + + This is checked by `tcCheckRecSelId` when checking `HsRecFld foo`. + +2. Check if the selector is applied to an argument that has a type + signature, for example: + + h = foo (s :: S) + + This is checked by `tcInferRecSelId`. + + +Updates are slightly more complex. The `disambiguateRecordBinds` +function tries to determine the parent datatype in three ways: + +1. Check for types that have all the fields being updated. For example: + + f x = x { foo = 3, bar = 2 } + + Here `f` must be updating `T` because neither `S` nor `U` have + both fields. This may also discover that no possible type exists. + For example the following will be rejected: + + f' x = x { foo = 3, baz = 3 } + +2. Use the type being pushed in, if it is already a TyConApp. The + following are valid updates to `T`: + + g :: T -> T + g x = x { foo = 3 } + + g' x = x { foo = 3 } :: T + +3. Use the type signature of the record expression, if it exists and + is a TyConApp. Thus this is valid update to `T`: + + h x = (x :: T) { foo = 3 } + + +Note that we do not look up the types of variables being updated, and +no constraint-solving is performed, so for example the following will +be rejected as ambiguous: + + let bad (s :: S) = foo s + + let r :: T + r = blah + in r { foo = 3 } + + \r. (r { foo = 3 }, r :: T ) + +We could add further tests, of a more heuristic nature. For example, +rather than looking for an explicit signature, we could try to infer +the type of the argument to a selector or the record expression being +updated, in case we are lucky enough to get a TyConApp straight +away. However, it might be hard for programmers to predict whether a +particular update is sufficiently obvious for the signature to be +omitted. Moreover, this might change the behaviour of typechecker in +non-obvious ways. + +See also Note [HsRecField and HsRecUpdField] in GHC.Hs.Pat. +-} + +tcInferRecSelId :: AmbiguousFieldOcc GhcRn + -> [HsExprArg 'TcpRn] -> Maybe TcRhoType + -> TcM (HsExpr GhcTc, TcSigmaType) +tcInferRecSelId (Unambiguous sel_name lbl) _args _mb_res_ty + = do { sel_id <- tc_rec_sel_id lbl sel_name + ; let expr = HsRecFld noExtField (Unambiguous sel_id lbl) + ; return (expr, idType sel_id) } + +tcInferRecSelId (Ambiguous _ lbl) args mb_res_ty + = do { sel_name <- tcInferAmbiguousRecSelId lbl args mb_res_ty + ; sel_id <- tc_rec_sel_id lbl sel_name + ; let expr = HsRecFld noExtField (Ambiguous sel_id lbl) + ; return (expr, idType sel_id) } + +------------------------ +tc_rec_sel_id :: Located RdrName -> Name -> TcM TcId +-- Like tc_infer_id, but returns an Id not a HsExpr, +-- so we can wrap it back up into a HsRecFld +tc_rec_sel_id lbl sel_name + = do { thing <- tcLookup sel_name + ; case thing of + ATcId { tct_id = id } + -> do { check_local_id occ id + ; return id } + + AGlobal (AnId id) + -> do { check_global_id occ id + ; return id } + -- A global cannot possibly be ill-staged + -- nor does it need the 'lifting' treatment + -- hence no checkTh stuff here + + _ -> failWithTc $ + ppr thing <+> text "used where a value identifier was expected" } + where + occ = rdrNameOcc (unLoc lbl) + +------------------------ +tcInferAmbiguousRecSelId :: Located RdrName + -> [HsExprArg 'TcpRn] -> Maybe TcRhoType + -> TcM Name +-- Disgusting special case for ambiguous record selectors +-- Given a RdrName that refers to multiple record fields, and the type +-- of its argument, try to determine the name of the selector that is +-- meant. +-- See Note [Disambiguating record fields] +tcInferAmbiguousRecSelId lbl args mb_res_ty + | arg1 : _ <- dropWhile (not . isVisibleArg) args -- A value arg is first + , EValArg { eva_arg = ValArg (L _ arg) } <- arg1 + , Just sig_ty <- obviousSig arg -- A type sig on the arg disambiguates + = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty + ; finish_ambiguous_selector lbl sig_tc_ty } + + | Just res_ty <- mb_res_ty + , Just (arg_ty,_) <- tcSplitFunTy_maybe res_ty + = finish_ambiguous_selector lbl (scaledThing arg_ty) + + | otherwise + = ambiguousSelector lbl + +finish_ambiguous_selector :: Located RdrName -> Type -> TcM Name +finish_ambiguous_selector lr@(L _ rdr) parent_type + = do { fam_inst_envs <- tcGetFamInstEnvs + ; case tyConOf fam_inst_envs parent_type of { + Nothing -> ambiguousSelector lr ; + Just p -> + + do { xs <- lookupParents rdr + ; let parent = RecSelData p + ; case lookup parent xs of { + Nothing -> failWithTc (fieldNotInType parent rdr) ; + Just gre -> + + do { addUsedGRE True gre + ; return (gre_name gre) } } } } } + +-- This field name really is ambiguous, so add a suitable "ambiguous +-- occurrence" error, then give up. +ambiguousSelector :: Located RdrName -> TcM a +ambiguousSelector (L _ rdr) + = do { addAmbiguousNameErr rdr + ; failM } + +-- | This name really is ambiguous, so add a suitable "ambiguous +-- occurrence" error, then continue +addAmbiguousNameErr :: RdrName -> TcM () +addAmbiguousNameErr rdr + = do { env <- getGlobalRdrEnv + ; let gres = lookupGRE_RdrName rdr env + ; setErrCtxt [] $ addNameClashErrRn rdr gres} + +-- A type signature on the argument of an ambiguous record selector or +-- the record expression in an update must be "obvious", i.e. the +-- outermost constructor ignoring parentheses. +obviousSig :: HsExpr GhcRn -> Maybe (LHsSigWcType GhcRn) +obviousSig (ExprWithTySig _ _ ty) = Just ty +obviousSig (HsPar _ p) = obviousSig (unLoc p) +obviousSig (HsPragE _ _ p) = obviousSig (unLoc p) +obviousSig _ = Nothing + +-- Extract the outermost TyCon of a type, if there is one; for +-- data families this is the representation tycon (because that's +-- where the fields live). +tyConOf :: FamInstEnvs -> TcSigmaType -> Maybe TyCon +tyConOf fam_inst_envs ty0 + = case tcSplitTyConApp_maybe ty of + Just (tc, tys) -> Just (fstOf3 (tcLookupDataFamInst fam_inst_envs tc tys)) + Nothing -> Nothing + where + (_, _, ty) = tcSplitSigmaTy ty0 + +-- Variant of tyConOf that works for ExpTypes +tyConOfET :: FamInstEnvs -> ExpRhoType -> Maybe TyCon +tyConOfET fam_inst_envs ty0 = tyConOf fam_inst_envs =<< checkingExpType_maybe ty0 + + +-- For an ambiguous record field, find all the candidate record +-- selectors (as GlobalRdrElts) and their parents. +lookupParents :: RdrName -> RnM [(RecSelParent, GlobalRdrElt)] +lookupParents rdr + = do { env <- getGlobalRdrEnv + ; let gres = lookupGRE_RdrName rdr env + ; mapM lookupParent gres } + where + lookupParent :: GlobalRdrElt -> RnM (RecSelParent, GlobalRdrElt) + lookupParent gre = do { id <- tcLookupId (gre_name gre) + ; if isRecordSelector id + then return (recordSelectorTyCon id, gre) + else failWithTc (notSelector (gre_name gre)) } + + +fieldNotInType :: RecSelParent -> RdrName -> SDoc +fieldNotInType p rdr + = unknownSubordinateErr (text "field of type" <+> quotes (ppr p)) rdr + +notSelector :: Name -> SDoc +notSelector field + = hsep [quotes (ppr field), text "is not a record selector"] + +naughtyRecordSel :: OccName -> SDoc +naughtyRecordSel lbl + = text "Cannot use record selector" <+> quotes (ppr lbl) <+> + text "as a function due to escaped type variables" $$ + text "Probable fix: use pattern-matching syntax instead" + + +{- ********************************************************************* +* * + Expressions with a type signature + expr :: type +* * +********************************************************************* -} + +tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn) + -> TcM (HsExpr GhcTc, TcSigmaType) +tcExprWithSig expr hs_ty + = do { sig_info <- checkNoErrs $ -- Avoid error cascade + tcUserTypeSig loc hs_ty Nothing + ; (expr', poly_ty) <- tcExprSig expr sig_info + ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) } + where + loc = getLoc (hsSigWcType hs_ty) + +tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType) +tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc }) + = setSrcSpan loc $ -- Sets the location for the implication constraint + do { let poly_ty = idType poly_id + ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty -> + tcCheckMonoExprNC expr rho_ty + ; return (mkLHsWrap wrap expr', poly_ty) } + +tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) + = setSrcSpan loc $ -- Sets the location for the implication constraint + do { (tclvl, wanted, (expr', sig_inst)) + <- pushLevelAndCaptureConstraints $ + do { sig_inst <- tcInstSig sig + ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $ + tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $ + tcCheckPolyExprNC expr (sig_inst_tau sig_inst) + ; return (expr', sig_inst) } + -- See Note [Partial expression signatures] + ; let tau = sig_inst_tau sig_inst + infer_mode | null (sig_inst_theta sig_inst) + , isNothing (sig_inst_wcx sig_inst) + = ApplyMR + | otherwise + = NoRestrictions + ; (qtvs, givens, ev_binds, residual, _) + <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted + ; emitConstraints residual + + ; tau <- zonkTcType tau + ; let inferred_theta = map evVarPred givens + tau_tvs = tyCoVarsOfType tau + ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta + tau_tvs qtvs (Just sig_inst) + ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau + my_sigma = mkInvisForAllTys binders (mkPhiTy my_theta tau) + ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis. + then return idHsWrapper -- Fast path; also avoids complaint when we infer + -- an ambiguous type and have AllowAmbiguousType + -- e..g infer x :: forall a. F a -> Int + else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma + + ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) + ; let poly_wrap = wrap + <.> mkWpTyLams qtvs + <.> mkWpLams givens + <.> mkWpLet ev_binds + ; return (mkLHsWrap poly_wrap expr', my_sigma) } + + +{- Note [Partial expression signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Partial type signatures on expressions are easy to get wrong. But +here is a guiding principile + e :: ty +should behave like + let x :: ty + x = e + in x + +So for partial signatures we apply the MR if no context is given. So + e :: IO _ apply the MR + e :: _ => IO _ do not apply the MR +just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan + +This makes a difference (#11670): + peek :: Ptr a -> IO CLong + peek ptr = peekElemOff undefined 0 :: _ +from (peekElemOff undefined 0) we get + type: IO w + constraints: Storable w + +We must NOT try to generalise over 'w' because the signature specifies +no constraints so we'll complain about not being able to solve +Storable w. Instead, don't generalise; then _ gets instantiated to +CLong, as it should. +-} + + +{- ********************************************************************* +* * + tcInferId, tcCheckId +* * +********************************************************************* -} + +tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc) +tcCheckId name res_ty + = do { (expr, actual_res_ty) <- tcInferId name + ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty]) + ; addFunResCtxt expr [] actual_res_ty res_ty $ + tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr + actual_res_ty res_ty } + +------------------------ +tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType) +-- Look up an occurrence of an Id +-- Do not instantiate its type +tcInferId id_name + | id_name `hasKey` assertIdKey + = do { dflags <- getDynFlags + ; if gopt Opt_IgnoreAsserts dflags + then tc_infer_id id_name + else tc_infer_assert id_name } + + | otherwise + = do { (expr, ty) <- tc_infer_id id_name + ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty) + ; return (expr, ty) } + +tc_infer_assert :: Name -> TcM (HsExpr GhcTc, TcSigmaType) +-- Deal with an occurrence of 'assert' +-- See Note [Adding the implicit parameter to 'assert'] +tc_infer_assert assert_name + = do { assert_error_id <- tcLookupId assertErrorName + ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name) + (idType assert_error_id) + ; return (mkHsWrap wrap (HsVar noExtField (noLoc assert_error_id)), id_rho) + } + +tc_infer_id :: Name -> TcM (HsExpr GhcTc, TcSigmaType) +tc_infer_id id_name + = do { thing <- tcLookup id_name + ; case thing of + ATcId { tct_id = id } + -> do { check_local_id occ id + ; return_id id } + + AGlobal (AnId id) + -> do { check_global_id occ id + ; return_id id } + + AGlobal (AConLike cl) -> case cl of + RealDataCon con -> return_data_con con + PatSynCon ps + | Just (expr, ty) <- patSynBuilderOcc ps + -> return (expr, ty) + | otherwise + -> nonBidirectionalErr id_name + + _ -> failWithTc $ + ppr thing <+> text "used where a value identifier was expected" } + where + occ = nameOccName id_name + + return_id id = return (HsVar noExtField (noLoc id), idType id) + + return_data_con con + = do { let tvs = dataConUserTyVarBinders con + theta = dataConOtherTheta con + args = dataConOrigArgTys con + res = dataConOrigResTy con + + -- See Note [Linear fields generalization] + ; mul_vars <- newFlexiTyVarTys (length args) multiplicityTy + ; let scaleArgs args' = zipWithEqual "return_data_con" combine mul_vars args' + combine var (Scaled One ty) = Scaled var ty + combine _ scaled_ty = scaled_ty + -- The combine function implements the fact that, as + -- described in Note [Linear fields generalization], if a + -- field is not linear (last line) it isn't made polymorphic. + + etaWrapper arg_tys = foldr (\scaled_ty wr -> WpFun WpHole wr scaled_ty empty) WpHole arg_tys + + -- See Note [Instantiating stupid theta] + ; let shouldInstantiate = (not (null (dataConStupidTheta con)) || + isKindLevPoly (tyConResKind (dataConTyCon con))) + ; case shouldInstantiate of + True -> do { (subst, tvs') <- newMetaTyVars (binderVars tvs) + ; let tys' = mkTyVarTys tvs' + theta' = substTheta subst theta + args' = substScaledTys subst args + res' = substTy subst res + ; wrap <- instCall (OccurrenceOf id_name) tys' theta' + ; let scaled_arg_tys = scaleArgs args' + eta_wrap = etaWrapper scaled_arg_tys + ; addDataConStupidTheta con tys' + ; return ( mkHsWrap (eta_wrap <.> wrap) + (HsConLikeOut noExtField (RealDataCon con)) + , mkVisFunTys scaled_arg_tys res') + } + False -> let scaled_arg_tys = scaleArgs args + wrap1 = mkWpTyApps (mkTyVarTys $ binderVars tvs) + eta_wrap = etaWrapper (map unrestricted theta ++ scaled_arg_tys) + wrap2 = mkWpTyLams $ binderVars tvs + in return ( mkHsWrap (wrap2 <.> eta_wrap <.> wrap1) + (HsConLikeOut noExtField (RealDataCon con)) + , mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res) + } + +check_local_id :: OccName -> Id -> TcM () +check_local_id occ id + = do { check_naughty occ id -- See Note [HsVar: naughty record selectors] + ; checkThLocalId id + ; tcEmitBindingUsage $ unitUE (idName id) One } + +check_global_id :: OccName -> Id -> TcM () +check_global_id occ id + = check_naughty occ id -- See Note [HsVar: naughty record selectors] + -- A global cannot possibly be ill-staged + -- nor does it need the 'lifting' treatment + -- Hence no checkTh stuff here + +check_naughty :: OccName -> TcId -> TcM () +check_naughty lbl id + | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl) + | otherwise = return () + +nonBidirectionalErr :: Outputable name => name -> TcM a +nonBidirectionalErr name = failWithTc $ + text "non-bidirectional pattern synonym" + <+> quotes (ppr name) <+> text "used in an expression" + +{- Note [HsVar: naughty record selectors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +All record selectors should really be HsRecFld (ambiguous or +unambiguous), but currently not all of them are: see #18452. So we +need to check for naughty record selectors in tc_infer_id, as well as +in tc_rec_sel_id. + +Remove this code when fixing #18452. + +Note [Linear fields generalization] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As per Note [Polymorphisation of linear fields], linear field of data +constructors get a polymorphic type when the data constructor is used as a term. + + Just :: forall {p} a. a #p-> Maybe a + +This rule is known only to the typechecker: Just keeps its linear type in Core. + +In order to desugar this generalised typing rule, we simply eta-expand: + + \a (x # p :: a) -> Just @a x + +has the appropriate type. We insert these eta-expansion with WpFun wrappers. + +A small hitch: if the constructor is levity-polymorphic (unboxed tuples, sums, +certain newtypes with -XUnliftedNewtypes) then this strategy produces + + \r1 r2 a b (x # p :: a) (y # q :: b) -> (# a, b #) + +Which has type + + forall r1 r2 a b. a #p-> b #q-> (# a, b #) + +Which violates the levity-polymorphism restriction see Note [Levity polymorphism +checking] in DsMonad. + +So we really must instantiate r1 and r2 rather than quantify over them. For +simplicity, we just instantiate the entire type, as described in Note +[Instantiating stupid theta]. It breaks visible type application with unboxed +tuples, sums and levity-polymorphic newtypes, but this doesn't appear to be used +anywhere. + +A better plan: let's force all representation variable to be *inferred*, so that +they are not subject to visible type applications. Then we can instantiate +inferred argument eagerly. + +Note [Adding the implicit parameter to 'assert'] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The typechecker transforms (assert e1 e2) to (assertError e1 e2). +This isn't really the Right Thing because there's no way to "undo" +if you want to see the original source code in the typechecker +output. We'll have fix this in due course, when we care more about +being able to reconstruct the exact original program. + + +Note [Instantiating stupid theta] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Normally, when we infer the type of an Id, we don't instantiate, +because we wish to allow for visible type application later on. +But if a datacon has a stupid theta, we're a bit stuck. We need +to emit the stupid theta constraints with instantiated types. It's +difficult to defer this to the lazy instantiation, because a stupid +theta has no spot to put it in a type. So we just instantiate eagerly +in this case. Thus, users cannot use visible type application with +a data constructor sporting a stupid theta. I won't feel so bad for +the users that complain. +-} + +{- +************************************************************************ +* * + Template Haskell checks +* * +************************************************************************ +-} + +checkThLocalId :: Id -> TcM () +-- The renamer has already done checkWellStaged, +-- in RnSplice.checkThLocalName, so don't repeat that here. +-- Here we just add constraints for cross-stage lifting +checkThLocalId id + = do { mb_local_use <- getStageAndBindLevel (idName id) + ; case mb_local_use of + Just (top_lvl, bind_lvl, use_stage) + | thLevel use_stage > bind_lvl + -> checkCrossStageLifting top_lvl id use_stage + _ -> return () -- Not a locally-bound thing, or + -- no cross-stage link + } + +-------------------------------------- +checkCrossStageLifting :: TopLevelFlag -> Id -> ThStage -> TcM () +-- If we are inside typed brackets, and (use_lvl > bind_lvl) +-- we must check whether there's a cross-stage lift to do +-- Examples \x -> [|| x ||] +-- [|| map ||] +-- +-- This is similar to checkCrossStageLifting in GHC.Rename.Splice, but +-- this code is applied to *typed* brackets. + +checkCrossStageLifting top_lvl id (Brack _ (TcPending ps_var lie_var q)) + | isTopLevel top_lvl + = when (isExternalName id_name) (keepAlive id_name) + -- See Note [Keeping things alive for Template Haskell] in GHC.Rename.Splice + + | otherwise + = -- Nested identifiers, such as 'x' in + -- E.g. \x -> [|| h x ||] + -- We must behave as if the reference to x was + -- h $(lift x) + -- We use 'x' itself as the splice proxy, used by + -- the desugarer to stitch it all back together. + -- If 'x' occurs many times we may get many identical + -- bindings of the same splice proxy, but that doesn't + -- matter, although it's a mite untidy. + do { let id_ty = idType id + ; checkTc (isTauTy id_ty) (polySpliceErr id) + -- If x is polymorphic, its occurrence sites might + -- have different instantiations, so we can't use plain + -- 'x' as the splice proxy name. I don't know how to + -- solve this, and it's probably unimportant, so I'm + -- just going to flag an error for now + + ; lift <- if isStringTy id_ty then + do { sid <- tcLookupId GHC.Builtin.Names.TH.liftStringName + -- See Note [Lifting strings] + ; return (HsVar noExtField (noLoc sid)) } + else + setConstraintVar lie_var $ + -- Put the 'lift' constraint into the right LIE + newMethodFromName (OccurrenceOf id_name) + GHC.Builtin.Names.TH.liftName + [getRuntimeRep id_ty, id_ty] + + -- Update the pending splices + ; ps <- readMutVar ps_var + ; let pending_splice = PendingTcSplice id_name + (nlHsApp (mkLHsWrap (applyQuoteWrapper q) (noLoc lift)) + (nlHsVar id)) + ; writeMutVar ps_var (pending_splice : ps) + + ; return () } + where + id_name = idName id + +checkCrossStageLifting _ _ _ = return () + +polySpliceErr :: Id -> SDoc +polySpliceErr id + = text "Can't splice the polymorphic local variable" <+> quotes (ppr id) + +{- +Note [Lifting strings] +~~~~~~~~~~~~~~~~~~~~~~ +If we see $(... [| s |] ...) where s::String, we don't want to +generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc. +So this conditional short-circuits the lifting mechanism to generate +(liftString "xy") in that case. I didn't want to use overlapping instances +for the Lift class in TH.Syntax, because that can lead to overlapping-instance +errors in a polymorphic situation. + +If this check fails (which isn't impossible) we get another chance; see +Note [Converting strings] in Convert.hs + +Local record selectors +~~~~~~~~~~~~~~~~~~~~~~ +Record selectors for TyCons in this module are ordinary local bindings, +which show up as ATcIds rather than AGlobals. So we need to check for +naughtiness in both branches. c.f. TcTyClsBindings.mkAuxBinds. +-} + + +{- ********************************************************************* +* * + Error reporting for function result mis-matches +* * +********************************************************************* -} + +addFunResCtxt :: HsExpr GhcTc -> [HsExprArg 'TcpTc] + -> TcType -> ExpRhoType + -> TcM a -> TcM a +-- When we have a mis-match in the return type of a function +-- try to give a helpful message about too many/few arguments +addFunResCtxt fun args fun_res_ty env_ty + = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg) + -- NB: use a landmark error context, so that an empty context + -- doesn't suppress some more useful context + where + mk_msg + = do { mb_env_ty <- readExpType_maybe env_ty + -- by the time the message is rendered, the ExpType + -- will be filled in (except if we're debugging) + ; fun_res' <- zonkTcType fun_res_ty + ; env' <- case mb_env_ty of + Just env_ty -> zonkTcType env_ty + Nothing -> + do { dumping <- doptM Opt_D_dump_tc_trace + ; MASSERT( dumping ) + ; newFlexiTyVarTy liftedTypeKind } + ; let -- See Note [Splitting nested sigma types in mismatched + -- function types] + (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res' + -- No need to call tcSplitNestedSigmaTys here, since env_ty is + -- an ExpRhoTy, i.e., it's already instantiated. + (_, _, env_tau) = tcSplitSigmaTy env' + (args_fun, res_fun) = tcSplitFunTys fun_tau + (args_env, res_env) = tcSplitFunTys env_tau + n_fun = length args_fun + n_env = length args_env + info | -- Check for too few args + -- fun_tau = a -> b, res_tau = Int + n_fun > n_env + , not_fun res_env + = text "Probable cause:" <+> quotes (ppr fun) + <+> text "is applied to too few arguments" + + | -- Check for too many args + -- fun_tau = a -> Int, res_tau = a -> b -> c -> d + -- The final guard suppresses the message when there + -- aren't enough args to drop; eg. the call is (f e1) + n_fun < n_env + , not_fun res_fun + , (n_fun + count isValArg args) >= n_env + -- Never suggest that a naked variable is + -- applied to too many args! + = text "Possible cause:" <+> quotes (ppr fun) + <+> text "is applied to too many arguments" + + | otherwise + = Outputable.empty + + ; return info } + where + not_fun ty -- ty is definitely not an arrow type, + -- and cannot conceivably become one + = case tcSplitTyConApp_maybe ty of + Just (tc, _) -> isAlgTyCon tc + Nothing -> False + +{- +Note [Splitting nested sigma types in mismatched function types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When one applies a function to too few arguments, GHC tries to determine this +fact if possible so that it may give a helpful error message. It accomplishes +this by checking if the type of the applied function has more argument types +than supplied arguments. + +Previously, GHC computed the number of argument types through tcSplitSigmaTy. +This is incorrect in the face of nested foralls, however! This caused Trac +#13311, for instance: + + f :: forall a. (Monoid a) => forall b. (Monoid b) => Maybe a -> Maybe b + +If one uses `f` like so: + + do { f; putChar 'a' } + +Then tcSplitSigmaTy will decompose the type of `f` into: + + Tyvars: [a] + Context: (Monoid a) + Argument types: [] + Return type: forall b. Monoid b => Maybe a -> Maybe b + +That is, it will conclude that there are *no* argument types, and since `f` +was given no arguments, it won't print a helpful error message. On the other +hand, tcSplitNestedSigmaTys correctly decomposes `f`'s type down to: + + Tyvars: [a, b] + Context: (Monoid a, Monoid b) + Argument types: [Maybe a] + Return type: Maybe b + +So now GHC recognizes that `f` has one more argument type than it was actually +provided. +-} + + +{- ********************************************************************* +* * + Misc utility functions +* * +********************************************************************* -} + +addLExprCtxt :: LHsExpr GhcRn -> TcRn a -> TcRn a +addLExprCtxt (L _ e) thing_inside = addExprCtxt e thing_inside + +addExprCtxt :: HsExpr GhcRn -> TcRn a -> TcRn a +addExprCtxt e thing_inside + = case e of + HsUnboundVar {} -> thing_inside + _ -> addErrCtxt (exprCtxt e) thing_inside + -- The HsUnboundVar special case addresses situations like + -- f x = _ + -- when we don't want to say "In the expression: _", + -- because it is mentioned in the error message itself + +exprCtxt :: HsExpr GhcRn -> SDoc +exprCtxt expr = hang (text "In the expression:") 2 (ppr (stripParensHsExpr expr)) + diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index d978f5dbf3..30fe0cad44 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -39,13 +39,14 @@ import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC , tcMonoExpr, tcMonoExprNC, tcExpr , tcCheckMonoExpr, tcCheckMonoExprNC - , tcCheckPolyExpr, tcCheckId ) + , tcCheckPolyExpr ) import GHC.Types.Basic (LexicalFixity(..)) import GHC.Hs import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Env import GHC.Tc.Gen.Pat +import GHC.Tc.Gen.Head( tcCheckId ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Gen.Bind diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index f01f67b39b..27b2b1358b 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -426,10 +426,9 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- Note [View patterns and polymorphism] -- Expression must be a function - ; let expr_orig = lexprCtOrigin expr - herald = text "A view pattern expression expects" + ; let herald = text "A view pattern expression expects" ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma) - <- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty + <- matchActualFunTySigma herald (Just (ppr expr)) (1,[]) expr_ty -- See Note [View patterns and polymorphism] -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma) diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 20538dd230..f29378122c 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -74,6 +74,8 @@ import GHC.Builtin.Utils import GHC.Types.Name.Reader import GHC.Tc.Utils.Zonk import GHC.Tc.Gen.Expr +import GHC.Tc.Errors( reportAllUnsolved ) +import GHC.Tc.Gen.App( tcInferSigma ) import GHC.Tc.Utils.Monad import GHC.Tc.Gen.Export import GHC.Tc.Types.Evidence @@ -99,6 +101,7 @@ import GHC.Tc.TyCl.Instance import GHC.IfaceToCore import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Instantiate (tcGetInsts) import GHC.Tc.Solver import GHC.Tc.TyCl import GHC.Tc.Instance.Typeable ( mkTypeableBinds ) @@ -136,7 +139,6 @@ import GHC.Data.FastString import GHC.Data.Maybe import GHC.Utils.Misc import GHC.Data.Bag -import GHC.Tc.Utils.Instantiate (tcGetInsts) import qualified GHC.LanguageExtensions as LangExt import Data.Data ( Data ) import GHC.Hs.Dump @@ -2478,9 +2480,9 @@ isGHCiMonad hsc_env ty Nothing -> failWithTc $ text ("Can't find type:" ++ ty) -- | How should we infer a type? See Note [TcRnExprMode] -data TcRnExprMode = TM_Inst -- ^ Instantiate the type fully (:type) - | TM_NoInst -- ^ Do not instantiate the type (:type +v) - | TM_Default -- ^ Default the type eagerly (:type +d) +data TcRnExprMode = TM_Inst -- ^ Instantiate inferred quantifiers only (:type) + | TM_Default -- ^ Instantiate all quantifiers, + -- and do eager defaulting (:type +d) -- | tcRnExpr just finds the type of an expression -- for :type @@ -2495,16 +2497,15 @@ tcRnExpr hsc_env mode rdr_expr (rn_expr, _fvs) <- rnLExpr rdr_expr ; failIfErrsM ; - -- Now typecheck the expression, and generalise its type - -- it might have a rank-2 type (e.g. :t runST) - uniq <- newUnique ; - let { fresh_it = itName uniq (getLoc rdr_expr) } ; - ((tclvl, (_tc_expr, res_ty)), lie) + -- Typecheck the expression + ((tclvl, res_ty), lie) <- captureTopConstraints $ pushTcLevelM $ - tc_infer rn_expr ; + tcInferSigma inst rn_expr ; -- Generalise + uniq <- newUnique ; + let { fresh_it = itName uniq (getLoc rdr_expr) } ; (qtvs, dicts, _, residual, _) <- simplifyInfer tclvl infer_mode [] {- No sig vars -} @@ -2528,14 +2529,10 @@ tcRnExpr hsc_env mode rdr_expr return (snd (normaliseType fam_envs Nominal ty)) } where - tc_infer expr | inst = tcInferRho expr - | otherwise = tcInferSigma expr - -- tcInferSigma: see Note [Implementing :type] - + -- Optionally instantiate the type of the expression -- See Note [TcRnExprMode] (inst, infer_mode, perhaps_disable_default_warnings) = case mode of - TM_Inst -> (True, NoRestrictions, id) - TM_NoInst -> (False, NoRestrictions, id) + TM_Inst -> (False, NoRestrictions, id) TM_Default -> (True, EagerDefaulting, unsetWOptM Opt_WarnTypeDefaults) {- Note [Implementing :type] @@ -2621,32 +2618,20 @@ tcRnType hsc_env flexi normalise rdr_type {- Note [TcRnExprMode] ~~~~~~~~~~~~~~~~~~~~~~ How should we infer a type when a user asks for the type of an expression e -at the GHCi prompt? We offer 3 different possibilities, described below. Each -considers this example, with -fprint-explicit-foralls enabled: - - foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String - :type{,-spec,-def} foo @Int +at the GHCi prompt? We offer 2 different possibilities, described below. Each +considers this example, with -fprint-explicit-foralls enabled. See also +https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0179-printing-foralls.rst :type / TM_Inst - In this mode, we report the type that would be inferred if a variable - were assigned to expression e, without applying the monomorphism restriction. - This means we instantiate the type and then regeneralize, as discussed - in #11376. + In this mode, we report the type obained by instantiating only the + /inferred/ quantifiers of e's type, solving constraints, and + re-generalising, as discussed in #11376. - > :type foo @Int - forall {b} {f :: * -> *}. (Foldable f, Num b) => Int -> f b -> String - - Note that the variables and constraints are reordered here, because this - is possible during regeneralization. Also note that the variables are - reported as Inferred instead of Specified. - -:type +v / TM_NoInst - - This mode is for the benefit of users using TypeApplications. It does no - instantiation whatsoever, sometimes meaning that class constraints are not - solved. + > :type reverse + reverse :: forall a. [a] -> [a] + -- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String > :type +v foo @Int forall f b. (Show Int, Num b, Foldable f) => Int -> f b -> String @@ -2655,12 +2640,17 @@ considers this example, with -fprint-explicit-foralls enabled: :type +d / TM_Default - This mode is for the benefit of users who wish to see instantiations of - generalized types, and in particular to instantiate Foldable and Traversable. - In this mode, any type variable that can be defaulted is defaulted. Because - GHCi uses -XExtendedDefaultRules, this means that Foldable and Traversable are + This mode is for the benefit of users who wish to see instantiations + of generalized types, and in particular to instantiate Foldable and + Traversable. In this mode, all type variables (inferred or + specified) are instantiated. Because GHCi uses + -XExtendedDefaultRules, this means that Foldable and Traversable are defaulted. + > :type +d reverse + reverse :: forall {a}. [a] -> [a] + + -- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String > :type +d foo @Int Int -> [Integer] -> String @@ -2676,6 +2666,10 @@ considers this example, with -fprint-explicit-foralls enabled: modified to include an element that is both Num and Monoid, the defaulting would succeed, of course.) + Note that the variables and constraints are reordered here, because this + is possible during regeneralization. Also note that the variables are + reported as Inferred instead of Specified. + Note [Kind-generalise in tcRnType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We switch on PolyKinds when kind-checking a user type, so that we will diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 557e56f48f..8cf326bac0 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -96,8 +96,8 @@ canonicalize (CNonCanonical { cc_ev = ev }) canEqNC ev eq_rel ty1 ty2 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred) canIrred OtherCIS ev - ForAllPred tvs theta p -> do traceTcS "canEvNC:forall" (ppr pred) - canForAllNC ev tvs theta p + ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred) + canForAllNC ev tvs th p where pred = ctEvPred ev @@ -708,11 +708,16 @@ canIrred status ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + do { -- Re-classify, in case flattening has improved its shape + -- Code is like the CNonCanonical case of canonicalize, except + -- that the IrredPred branch stops work ; case classifyPredType (ctEvPred new_ev) of ClassPred cls tys -> canClassNC new_ev cls tys EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2 - _ -> continueWith $ + ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred) + canForAllNC ev tvs th p + IrredPred {} -> continueWith $ mkIrredCt status new_ev } } {- ********************************************************************* @@ -2106,6 +2111,10 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs ; continueWith (mkIrredCt status new_ev) } where mtvu = metaTyVarUpdateOK dflags tv1 rhs + -- Despite the name of the function, tv1 may not be a + -- unification variable; we are really checking that this + -- equality is ok to be used to rewrite others, i.e. that + -- it satisfies the conditions for CTyEqCan role = eqRelRole eq_rel @@ -2135,7 +2144,7 @@ k2 and use this to cast. To wit, from [X] (tv :: k1) ~ (rhs :: k2) -we go to +(where [X] is [G], [W], or [D]), we go to [noDerived X] co :: k2 ~ k1 [X] (tv :: k1) ~ ((rhs |> co) :: k1) @@ -2145,6 +2154,9 @@ where noDerived G = G noDerived _ = W +For Wanted/Derived, the [X] constraint is "blocked" (not CTyEqCan, is CIrred) +until the k1~k2 constraint solved: Wrinkle (2). + Wrinkles: (1) The noDerived step is because Derived equalities have no evidence. @@ -2157,7 +2169,7 @@ Wrinkles: [W] (tv :: k1) ~ ((rhs |> co) :: k1) as canonical in the inert set. In particular, we must not unify tv. If we did, the Wanted becomes a Given (effectively), and then can - rewrite other Wanteds. But that's bad: See Note [Wanteds to not rewrite Wanteds] + rewrite other Wanteds. But that's bad: See Note [Wanteds do not rewrite Wanteds] in GHC.Tc.Types.Constraint. The problem is about poor error messages. See #11198 for tales of destruction. diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index a99ab10404..88a0e4eeef 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -15,8 +15,7 @@ module GHC.Tc.TyCl.PatSyn ( tcPatSynDecl , tcPatSynBuilderBind - , tcPatSynBuilderOcc - , nonBidirectionalErr + , patSynBuilderOcc ) where @@ -884,13 +883,12 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name add_dummy_arg other_mg = pprPanic "add_dummy_arg" $ pprMatches other_mg -tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTc, TcSigmaType) --- monadic only for failure -tcPatSynBuilderOcc ps - | Just (builder_id, add_void_arg) <- builder +patSynBuilderOcc :: PatSyn -> Maybe (HsExpr GhcTc, TcSigmaType) +patSynBuilderOcc ps + | Just (builder_id, add_void_arg) <- patSynBuilder ps , let builder_expr = HsConLikeOut noExtField (PatSynCon ps) builder_ty = idType builder_id - = return $ + = Just $ if add_void_arg then ( builder_expr -- still just return builder_expr; the void# arg is added -- by dsConLike in the desugarer @@ -898,10 +896,7 @@ tcPatSynBuilderOcc ps else (builder_expr, builder_ty) | otherwise -- Unidirectional - = nonBidirectionalErr name - where - name = patSynName ps - builder = patSynBuilder ps + = Nothing add_void :: Bool -> Type -> Type add_void need_dummy_arg ty @@ -1091,11 +1086,6 @@ want to avoid difficult to decipher core lint errors! -} -nonBidirectionalErr :: Outputable name => name -> TcM a -nonBidirectionalErr name = failWithTc $ - text "non-bidirectional pattern synonym" - <+> quotes (ppr name) <+> text "used in an expression" - -- Walk the whole pattern and for all ConPatOuts, collect the -- existentially-bound type variables and evidence binding variables. -- diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot index fb4ac51013..38fc4b52f1 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs-boot +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs-boot @@ -3,7 +3,6 @@ module GHC.Tc.TyCl.PatSyn where import GHC.Hs ( PatSynBind, LHsBinds ) import GHC.Tc.Types ( TcM, TcSigInfo ) import GHC.Tc.Utils.Monad ( TcGblEnv) -import GHC.Utils.Outputable ( Outputable ) import GHC.Hs.Extension ( GhcRn, GhcTc ) import Data.Maybe ( Maybe ) @@ -13,4 +12,3 @@ tcPatSynDecl :: PatSynBind GhcRn GhcRn tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn -> TcM (LHsBinds GhcTc) -nonBidirectionalErr :: Outputable name => name -> TcM a diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs index e7b067e946..0528976a6b 100644 --- a/compiler/GHC/Tc/TyCl/Utils.hs +++ b/compiler/GHC/Tc/TyCl/Utils.hs @@ -1095,9 +1095,4 @@ Therefore, when used in the right-hand side of `unT`, GHC attempts to instantiate `a` with `(forall b. b -> b) -> Int`, which is impredicative. To make sure that GHC is OK with this, we enable ImpredicativeTypes interally when typechecking these HsBinds so that the user does not have to. - -Although ImpredicativeTypes is somewhat fragile and unpredictable in GHC right -now, it will become robust when Quick Look impredicativity is implemented. In -the meantime, using ImpredicativeTypes to instantiate the `a` type variable in -recSelError's type does actually work, so its use here is benign. -} diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index d93e8fc84f..0e928ed5fd 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -12,7 +12,7 @@ module GHC.Tc.Utils.Instantiate ( topSkolemise, - topInstantiate, topInstantiateInferred, + topInstantiate, instantiateSigma, instCall, instDFunType, instStupidTheta, instTyVarsWith, newWanted, newWanteds, @@ -72,6 +72,7 @@ import GHC.Types.Name import GHC.Types.Var import GHC.Core.DataCon import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Builtin.Names import GHC.Types.SrcLoc as SrcLoc import GHC.Driver.Session @@ -189,66 +190,44 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- and e :: ty -- then wrap e :: rho (that is, wrap :: ty "->" rho) -- NB: always returns a rho-type, with no top-level forall or (=>) -topInstantiate = top_instantiate True +topInstantiate orig ty + | (tvs, theta, body) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (_, wrap1, body1) <- instantiateSigma orig tvs theta body --- | Instantiate all outer 'Inferred' binders --- and any context. Never looks through arrows or specified type variables. --- Used for visible type application. -topInstantiateInferred :: CtOrigin -> TcSigmaType - -> TcM (HsWrapper, TcSigmaType) --- if topInstantiate ty = (wrap, rho) --- and e :: ty --- then wrap e :: rho --- NB: may return a sigma-type -topInstantiateInferred = top_instantiate False - -top_instantiate :: Bool -- True <=> instantiate *all* variables - -- False <=> instantiate only the inferred ones - -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -top_instantiate inst_all orig ty - | (binders, phi) <- tcSplitForAllVarBndrs ty - , (theta, rho) <- tcSplitPhiTy phi - , not (null binders && null theta) - = do { let (inst_bndrs, leave_bndrs) = span should_inst binders - (inst_theta, leave_theta) - | null leave_bndrs = (theta, []) - | otherwise = ([], theta) - in_scope = mkInScopeSet (tyCoVarsOfType ty) - empty_subst = mkEmptyTCvSubst in_scope - inst_tvs = binderVars inst_bndrs - ; (subst, inst_tvs') <- mapAccumLM newMetaTyVarX empty_subst inst_tvs - ; let inst_theta' = substTheta subst inst_theta - sigma' = substTy subst (mkForAllTys leave_bndrs $ - mkPhiTy leave_theta rho) - inst_tv_tys' = mkTyVarTys inst_tvs' - - ; wrap1 <- instCall orig inst_tv_tys' inst_theta' - ; traceTc "Instantiating" - (vcat [ text "all tyvars?" <+> ppr inst_all - , text "origin" <+> pprCtOrigin orig - , text "type" <+> debugPprType ty - , text "theta" <+> ppr theta - , text "leave_bndrs" <+> ppr leave_bndrs - , text "with" <+> vcat (map debugPprType inst_tv_tys') - , text "theta:" <+> ppr inst_theta' ]) - - ; (wrap2, rho2) <- - if null leave_bndrs -- NB: if inst_all is True then leave_bndrs = [] + -- Loop, to account for types like + -- forall a. Num a => forall b. Ord b => ... + ; (wrap2, rho) <- topInstantiate orig body1 - -- account for types like forall a. Num a => forall b. Ord b => ... - then top_instantiate inst_all orig sigma' + ; return (wrap2 <.> wrap1, rho) } - -- but don't loop if there were any un-inst'able tyvars - else return (idHsWrapper, sigma') + | otherwise = return (idHsWrapper, ty) - ; return (wrap2 <.> wrap1, rho2) } +instantiateSigma :: CtOrigin -> [TyVar] -> TcThetaType -> TcSigmaType + -> TcM ([TcTyVar], HsWrapper, TcSigmaType) +-- (instantiate orig tvs theta ty) +-- instantiates the the type variables tvs, emits the (instantiated) +-- constraints theta, and returns the (instantiated) type ty +instantiateSigma orig tvs theta body_ty + = do { (subst, inst_tvs) <- mapAccumLM newMetaTyVarX empty_subst tvs + ; let inst_theta = substTheta subst theta + inst_body = substTy subst body_ty + inst_tv_tys = mkTyVarTys inst_tvs + + ; wrap <- instCall orig inst_tv_tys inst_theta + ; traceTc "Instantiating" + (vcat [ text "origin" <+> pprCtOrigin orig + , text "tvs" <+> ppr tvs + , text "theta" <+> ppr theta + , text "type" <+> debugPprType body_ty + , text "with" <+> vcat (map debugPprType inst_tv_tys) + , text "theta:" <+> ppr inst_theta ]) - | otherwise = return (idHsWrapper, ty) + ; return (inst_tvs, wrap, inst_body) } where - - should_inst bndr - | inst_all = True - | otherwise = binderArgFlag bndr == Inferred + free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta + in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs) + empty_subst = mkEmptyTCvSubst in_scope instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst -- Use this when you want to instantiate (forall a b c. ty) with diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 0995eb51e9..62e39879d7 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -801,10 +801,11 @@ influences the way it is tidied; see TypeRep.tidyTyVarBndr. metaInfoToTyVarName :: MetaInfo -> FastString metaInfoToTyVarName meta_info = case meta_info of - TauTv -> fsLit "t" - FlatMetaTv -> fsLit "fmv" - FlatSkolTv -> fsLit "fsk" - TyVarTv -> fsLit "a" + TauTv -> fsLit "t" + FlatMetaTv -> fsLit "fmv" + FlatSkolTv -> fsLit "fsk" + TyVarTv -> fsLit "a" + RuntimeUnkTv -> fsLit "r" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 21b6b962d9..6d5ef37442 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/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, + tcSplitForAllTys, tcSplitSomeForAllTys, tcSplitForAllTysReq, tcSplitForAllTysInvis, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, tcSplitPhiTy, tcSplitPredFunTy_maybe, @@ -561,6 +561,9 @@ data MetaInfo -- It is filled in /only/ by unflattenGivens -- See Note [The flattening story] in GHC.Tc.Solver.Flatten + | RuntimeUnkTv -- A unification variable used in the GHCi debugger. + -- It /is/ allowed to unify with a polytype, unlike TauTv + instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty @@ -570,6 +573,7 @@ instance Outputable MetaInfo where ppr TyVarTv = text "tyv" ppr FlatMetaTv = text "fmv" ppr FlatSkolTv = text "fsk" + ppr RuntimeUnkTv = text "rutv" {- ********************************************************************* * * @@ -1222,6 +1226,19 @@ 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. +tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyVar], Type) +tcSplitSomeForAllTys argf_pred ty + = split ty ty [] + where + split _ (ForAllTy (Bndr tv argf) ty) tvs + | argf_pred argf = split ty ty (tv:tvs) + split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs + split orig_ty _ tvs = (reverse tvs, orig_ty) + -- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type -- variable binders. All split tyvars are annotated with '()'. tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type) diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 6a83348b2a..0c29a6557f 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -32,8 +32,8 @@ module GHC.Tc.Utils.Unify ( matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, - matchActualFunTysRho, matchActualFunTySigma, matchExpectedFunKind, + matchActualFunTySigma, matchActualFunTysRho, metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) @@ -69,13 +69,155 @@ import GHC.Driver.Session import GHC.Types.Basic import GHC.Data.Bag import GHC.Utils.Misc -import qualified GHC.LanguageExtensions as LangExt import GHC.Utils.Outputable as Outputable import GHC.Utils.Panic import Control.Monad import Control.Arrow ( second ) + +{- ********************************************************************* +* * + matchActualFunTys +* * +********************************************************************* -} + +-- | matchActualFunTySigma does looks for just one function arrow +-- returning an uninstantiated sigma-type +matchActualFunTySigma + :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> Maybe SDoc -- The thing with type TcSigmaType + -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and + -- types of values args to which function has + -- been applied already (reversed) + -- Both are used only for error messages) + -> TcRhoType -- Type to analyse: a TcRhoType + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) +-- The /argument/ is a RhoType +-- The /result/ is an (uninstantiated) SigmaType +-- +-- See Note [matchActualFunTy error handling] for the first three arguments + +-- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty +-- then wrap :: fun_ty ~> (arg_ty -> res_ty) +-- and NB: res_ty is an (uninstantiated) SigmaType + +matchActualFunTySigma herald mb_thing err_info fun_ty + = ASSERT2( isRhoTy fun_ty, ppr fun_ty ) + go fun_ty + where + -- Does not allocate unnecessary meta variables: if the input already is + -- a function, we just take it apart. Not only is this efficient, + -- it's important for higher rank: the argument might be of form + -- (forall a. ty) -> other + -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd + -- hide the forall inside a meta-variable + go :: TcRhoType -- The type we're processing, perhaps after + -- expanding any type synonym + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) + go ty | Just ty' <- tcView ty = go ty' + + go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) + = ASSERT( af == VisArg ) + return (idHsWrapper, Scaled w arg_ty, res_ty) + + go ty@(TyVarTy tv) + | isMetaTyVar tv + = do { cts <- readMetaTyVar tv + ; case cts of + Indirect ty' -> go ty' + Flexi -> defer ty } + + -- In all other cases we bale out into ordinary unification + -- However unlike the meta-tyvar case, we are sure that the + -- number of arguments doesn't match arity of the original + -- type, so we can add a bit more context to the error message + -- (cf #7869). + -- + -- It is not always an error, because specialized type may have + -- different arity, for example: + -- + -- > f1 = f2 'a' + -- > f2 :: Monad m => m Bool + -- > f2 = undefined + -- + -- But in that case we add specialized type into error context + -- anyway, because it may be useful. See also #9605. + go ty = addErrCtxtM (mk_ctxt ty) (defer ty) + + ------------ + defer fun_ty + = do { arg_ty <- newOpenFlexiTyVarTy + ; res_ty <- newOpenFlexiTyVarTy + ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty + ; co <- unifyType mb_thing fun_ty unif_fun_ty + ; return (mkWpCastN co, unrestricted arg_ty, res_ty) } + + ------------ + mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far) + res_ty n_val_args_in_call + (n_val_args_in_call, arg_tys_so_far) = err_info + +{- Note [matchActualFunTy error handling] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +matchActualFunTySigma is made much more complicated by the +desire to produce good error messages. Consider the application + f @Int x y +In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments, +and then call matchActualFunTysPart for each individual value +argument. It, in turn, must instantiate any type/dictionary args, +before looking for an arrow type. + +But if it doesn't find an arrow type, it wants to generate a message +like "f is applied to two arguments but its type only has one". +To do that, it needs to konw about the args that tcArgs has already +munched up -- hence passing in n_val_args_in_call and arg_tys_so_far; +and hence also the accumulating so_far arg to 'go'. + +This allows us (in mk_ctxt) to construct f's /instantiated/ type, +with just the values-arg arrows, which is what we really want +in the error message. + +Ugh! +-} + +-- Like 'matchExpectedFunTys', but used when you have an "actual" type, +-- for example in function application +matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Maybe SDoc -- the thing with type TcSigmaType + -> Arity + -> TcSigmaType + -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType) +-- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) +-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) +-- and res_ty is a RhoType +-- NB: the returned type is top-instantiated; it's a RhoType +matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty + = go n_val_args_wanted [] fun_ty + where + go n so_far fun_ty + | not (isRhoTy fun_ty) + = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty + ; (wrap2, arg_tys, res_ty) <- go n so_far rho + ; return (wrap2 <.> wrap1, arg_tys, res_ty) } + + go 0 _ fun_ty = return (idHsWrapper, [], fun_ty) + + go n so_far fun_ty + = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma + herald mb_thing + (n_val_args_wanted, so_far) + fun_ty + ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 + ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc + ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } + where + doc = text "When inferring the argument type of a function with type" <+> + quotes (ppr fun_ty) + + {- ************************************************************************ * * @@ -226,167 +368,32 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside ------------ mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) mk_ctxt arg_tys res_ty env - = do { (env', ty) <- zonkTidyTcType env (mkVisFunTys arg_tys' res_ty) - ; return ( env', mk_fun_tys_msg herald ty arity) } + = mkFunTysMsg env herald arg_tys' res_ty arity where - arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) (reverse arg_tys) + arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $ + reverse arg_tys -- this is safe b/c we're called from "go" --- Like 'matchExpectedFunTys', but used when you have an "actual" type, --- for example in function application -matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType - -> Arity - -> TcSigmaType - -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType) --- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) --- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) --- and res_ty is a RhoType --- NB: the returned type is top-instantiated; it's a RhoType -matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty - = go n_val_args_wanted [] fun_ty - where - go 0 _ fun_ty - = do { (wrap, rho) <- topInstantiate ct_orig fun_ty - ; return (wrap, [], rho) } - go n so_far fun_ty - = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma - herald ct_orig mb_thing - (n_val_args_wanted, so_far) - fun_ty - ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 - ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc - ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr fun_ty) - --- | matchActualFunTySigm does looks for just one function arrow --- returning an uninstantiated sigma-type -matchActualFunTySigma - :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType - -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and - -- types of values args to which function has - -- been applied already (reversed) - -- Both are used only for error messages) - -> TcSigmaType -- Type to analyse - -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) --- See Note [matchActualFunTys error handling] for all these arguments - --- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty --- then wrap :: fun_ty ~> (arg_ty -> res_ty) --- and NB: res_ty is an (uninstantiated) SigmaType - -matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty - = go fun_ty --- Does not allocate unnecessary meta variables: if the input already is --- a function, we just take it apart. Not only is this efficient, --- it's important for higher rank: the argument might be of form --- (forall a. ty) -> other --- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd --- hide the forall inside a meta-variable - --- (*) Sometimes it's necessary to call matchActualFunTys with only part --- (that is, to the right of some arrows) of the type of the function in --- question. (See GHC.Tc.Gen.Expr.tcArgs.) This argument is the reversed list of --- arguments already seen (that is, not part of the TcSigmaType passed --- in elsewhere). +mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity + -> TcM (TidyEnv, MsgDoc) +mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call + = do { (env', fun_rho) <- zonkTidyTcType env $ + mkVisFunTys arg_tys res_ty - where - go :: TcSigmaType -- The remainder of the type as we're processing - -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) - go ty | Just ty' <- tcView ty = go ty' + ; let (all_arg_tys, _) = splitFunTys fun_rho + n_fun_args = length all_arg_tys - go ty - | not (null tvs && null theta) - = do { (wrap1, rho) <- topInstantiate ct_orig ty - ; (wrap2, arg_ty, res_ty) <- go rho - ; return (wrap2 <.> wrap1, arg_ty, res_ty) } - where - (tvs, theta, _) = tcSplitSigmaTy ty - - go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) - = ASSERT( af == VisArg ) - return (idHsWrapper, Scaled w arg_ty, res_ty) + msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end + = text "In the result of a function call" + | otherwise + = hang (full_herald <> comma) + 2 (sep [ text "but its type" <+> quotes (pprType fun_rho) + , if n_fun_args == 0 then text "has none" + else text "has only" <+> speakN n_fun_args]) - go ty@(TyVarTy tv) - | isMetaTyVar tv - = do { cts <- readMetaTyVar tv - ; case cts of - Indirect ty' -> go ty' - Flexi -> defer ty } - - -- In all other cases we bale out into ordinary unification - -- However unlike the meta-tyvar case, we are sure that the - -- number of arguments doesn't match arity of the original - -- type, so we can add a bit more context to the error message - -- (cf #7869). - -- - -- It is not always an error, because specialized type may have - -- different arity, for example: - -- - -- > f1 = f2 'a' - -- > f2 :: Monad m => m Bool - -- > f2 = undefined - -- - -- But in that case we add specialized type into error context - -- anyway, because it may be useful. See also #9605. - go ty = addErrCtxtM (mk_ctxt ty) (defer ty) - - ------------ - defer fun_ty - = do { arg_ty <- newOpenFlexiTyVarTy - ; res_ty <- newOpenFlexiTyVarTy - ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty - ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; return (mkWpCastN co, unrestricted arg_ty, res_ty) } - - ------------ - mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt res_ty env - = do { (env', ty) <- zonkTidyTcType env $ - mkVisFunTys (reverse arg_tys_so_far) res_ty - ; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) } - (n_val_args_in_call, arg_tys_so_far) = err_info - -mk_fun_tys_msg :: SDoc -> TcType -> Arity -> SDoc -mk_fun_tys_msg herald ty n_args_in_call - | n_args_in_call <= n_fun_args -- Enough args, in the end - = text "In the result of a function call" - | otherwise - = hang (herald <+> speakNOf n_args_in_call (text "value argument") <> comma) - 2 (sep [ text "but its type" <+> quotes (pprType ty) - , if n_fun_args == 0 then text "has none" - else text "has only" <+> speakN n_fun_args]) - where - (args, _) = tcSplitFunTys ty - n_fun_args = length args - -{- Note [matchActualFunTys error handling] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -matchActualFunTysPart is made much more complicated by the -desire to produce good error messages. Consider the application - f @Int x y -In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments, -and then call matchActualFunTysPart for each individual value -argument. It, in turn, must instantiate any type/dictionary args, -before looking for an arrow type. - -But if it doesn't find an arrow type, it wants to generate a message -like "f is applied to two arguments but its type only has one". -To do that, it needs to konw about the args that tcArgs has already -munched up -- hence passing in n_val_args_in_call and arg_tys_so_far; -and hence also the accumulating so_far arg to 'go'. - -This allows us (in mk_ctxt) to construct f's /instantiated/ type, -with just the values-arg arrows, which is what we really want -in the error message. - -Ugh! --} + ; return (env', msg) } + where + full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument") ---------------------- matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType) @@ -519,7 +526,7 @@ tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpR tcWrapResultO orig rn_expr expr actual_ty res_ty = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty , text "Expected:" <+> ppr res_ty ]) - ; wrap <- tcSubTypeNC orig GenSigCtxt (Just rn_expr) actual_ty res_ty + ; wrap <- tcSubTypeNC orig GenSigCtxt (Just (ppr rn_expr)) actual_ty res_ty ; return (mkHsWrap wrap expr) } tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc @@ -533,7 +540,7 @@ tcWrapResultMono rn_expr expr act_ty res_ty = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr ) do { co <- case res_ty of Infer inf_res -> fillInferResult act_ty inf_res - Check exp_ty -> unifyType (Just rn_expr) act_ty exp_ty + Check exp_ty -> unifyType (Just (ppr rn_expr)) act_ty exp_ty ; return (mkHsWrapCo co expr) } ------------------------ @@ -565,7 +572,7 @@ tcSubType orig ctxt ty_actual ty_expected tcSubTypeNC :: CtOrigin -- Used when instantiating -> UserTypeCtxt -- Used when skolemising - -> Maybe (HsExpr GhcRn) -- The expression that has type 'actual' (if known) + -> Maybe SDoc -- The expression that has type 'actual' (if known) -> TcSigmaType -- Actual type -> ExpRhoType -- Expected type -> TcM HsWrapper @@ -661,12 +668,7 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected ; return (sk_wrap <.> inner_wrap) } where - possibly_poly ty - | isForAllTy ty = True - | Just (_, _, res) <- splitFunTy_maybe ty = possibly_poly res - | otherwise = False - -- NB *not* tcSplitFunTy, because here we want - -- to decompose type-class arguments too + possibly_poly ty = not (isRhoTy ty) definitely_poly ty | (tvs, theta, tau) <- tcSplitSigmaTy ty @@ -719,9 +721,6 @@ So roughly: then we can revert to simple equality. But we need to be careful. These examples are all fine: - * (Char -> forall a. a->a) <= (forall a. Char -> a -> a) - Polymorphism is buried in ty_actual - * (Char->Char) <= (forall a. Char -> Char) ty_expected isn't really polymorphic @@ -832,10 +831,11 @@ to checkConstraints. tcSkolemiseScoped is very similar, but differs in two ways: -* It deals specially with just the outer forall, bringing those - type variables into lexical scope. To my surprise, I found that - doing this regardless (in tcSkolemise) caused a non-trivial (1%-ish) - perf hit on the compiler. +* It deals specially with just the outer forall, bringing those type + variables into lexical scope. To my surprise, I found that doing + this unconditionally in tcSkolemise (i.e. doing it even if we don't + need to bring the variables into lexical scope, which is harmless) + caused a non-trivial (1%-ish) perf hit on the compiler. * It always calls checkConstraints, even if there are no skolem variables at all. Reason: there might be nested deferred errors @@ -848,6 +848,8 @@ tcSkolemise, tcSkolemiseScoped -> (TcType -> TcM result) -> TcM (HsWrapper, result) -- ^ The wrapper has type: spec_ty ~> expected_ty +-- See Note [Skolemisation] for the differences between +-- tcSkolemiseScoped and tcSkolemise tcSkolemiseScoped ctxt expected_ty thing_inside = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty @@ -1039,7 +1041,7 @@ take care: [W] C Int b2 -- from g_blan and fundpes can yield [D] b1 ~ b2, even though the two functions have literally nothing to do with each other. #14185 is an example. - Building an implication keeps them separage. + Building an implication keeps them separate. -} {- @@ -1053,8 +1055,9 @@ The exported functions are all defined as versions of some non-exported generic functions. -} -unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' - -> TcTauType -> TcTauType -> TcM TcCoercionN +unifyType :: Maybe SDoc -- ^ If present, the thing that has type ty1 + -> TcTauType -> TcTauType -- ty1, ty2 + -> TcM TcCoercionN -- :: ty1 ~# ty2 -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 @@ -1077,13 +1080,13 @@ unifyTypeET ty1 ty2 , uo_visible = True } -unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN -unifyKind thing ty1 ty2 +unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN +unifyKind mb_thing ty1 ty2 = uType KindLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 - , uo_thing = ppr <$> thing + , uo_thing = mb_thing , uo_visible = True } @@ -1186,10 +1189,12 @@ uType t_or_k origin orig_ty1 orig_ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - -- Functions (or predicate functions) just check the two parts - go (FunTy _ w1 fun1 arg1) (FunTy _ w2 fun2 arg2) - = do { co_l <- uType t_or_k origin fun1 fun2 - ; co_r <- uType t_or_k origin arg1 arg2 + -- Functions (t1 -> t2) just check the two parts + -- Do not attempt (c => t); just defer + go (FunTy { ft_af = VisArg, ft_mult = w1, ft_arg = arg1, ft_res = res1 }) + (FunTy { ft_af = VisArg, ft_mult = w2, ft_arg = arg2, ft_res = res2 }) + = do { co_l <- uType t_or_k origin arg1 arg2 + ; co_r <- uType t_or_k origin res1 res2 ; co_w <- uType t_or_k origin w1 w2 ; return $ mkFunCo Nominal co_w co_l co_r } @@ -1479,6 +1484,7 @@ swapOverTyVars is_given tv1 tv2 lhsPriority :: TcTyVar -> Int -- Higher => more important to be on the LHS +-- => more likely to be eliminated -- See Note [TyVar/TyVar orientation] lhsPriority tv = ASSERT2( isTyVar tv, ppr tv) @@ -1486,10 +1492,12 @@ lhsPriority tv RuntimeUnk -> 0 SkolemTv {} -> 0 MetaTv { mtv_info = info } -> case info of - FlatSkolTv -> 1 - TyVarTv -> 2 - TauTv -> 3 - FlatMetaTv -> 4 + FlatSkolTv -> 1 + TyVarTv -> 2 + TauTv -> 3 + FlatMetaTv -> 4 + RuntimeUnkTv -> 5 + {- Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? @@ -1855,7 +1863,7 @@ matchExpectedFunKind hs_ty n k = go n k Indirect fun_kind -> go n fun_kind Flexi -> defer n k } - go n (FunTy _ w arg res) + go n (FunTy { ft_mult = w, ft_arg = arg, ft_res = res }) = do { co <- go (n-1) res ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) } @@ -1943,7 +1951,7 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () -- a) the given variable occurs in the given type. -- b) there is a forall in the type (unless we have -XImpredicativeTypes) occCheckForErrors dflags tv ty - = case preCheck dflags True tv ty of + = case mtvu_check dflags True tv ty of MTVU_OK _ -> MTVU_OK () MTVU_Bad -> MTVU_Bad MTVU_HoleBlocker -> MTVU_HoleBlocker @@ -1957,13 +1965,20 @@ metaTyVarUpdateOK :: DynFlags -> TcType -- ty :: k2 -> MetaTyVarUpdateResult TcType -- possibly-expanded ty -- (metaTyVarUpdateOK tv ty) --- We are about to update the meta-tyvar tv with ty --- Check (a) that tv doesn't occur in ty (occurs check) +-- Checks that the equality tv~ty is OK to be used to rewrite +-- other equalities. Equivalently, checks the conditions for CTyEqCan +-- (a) that tv doesn't occur in ty (occurs check) -- (b) that ty does not have any foralls -- (in the impredicative case), or type functions -- (c) that ty does not have any blocking coercion holes -- See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical" -- +-- Used in two places: +-- - In the eager unifier: uUnfilledVar2 +-- - In the canonicaliser: GHC.Tc.Solver.Canonical.canEqTyVar2 +-- Note that in the latter case tv is not necessarily a meta-tyvar, +-- despite the name of this function. + -- We have two possible outcomes: -- (1) Return the type to update the type variable with, -- [we know the update is ok] @@ -1982,7 +1997,7 @@ metaTyVarUpdateOK :: DynFlags -- See Note [Refactoring hazard: checkTauTvUpdate] metaTyVarUpdateOK dflags tv ty - = case preCheck dflags False tv ty of + = case mtvu_check dflags False tv ty of -- False <=> type families not ok -- See Note [Prevent unification with type families] MTVU_OK _ -> MTVU_OK ty @@ -1992,11 +2007,11 @@ metaTyVarUpdateOK dflags tv ty Just expanded_ty -> MTVU_OK expanded_ty Nothing -> MTVU_Occurs -preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () --- A quick check for --- (a) a forall type (unless -XImpredicativeTypes) --- (b) a predicate type (unless -XImpredicativeTypes) --- (c) a type family +mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () +-- Checks the invariants for CTyEqCan. In particular: +-- (a) a forall type (forall a. blah) +-- (b) a predicate type (c => ty) +-- (c) a type family; see Note [Prevent unification with type families] -- (d) a blocking coercion hole -- (e) an occurrence of the type variable (occurs check) -- @@ -2004,15 +2019,20 @@ preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () -- inside the kinds of variables it mentions. For (d) we look deeply -- in coercions, and for (e) we do look in the kinds of course. -preCheck dflags ty_fam_ok tv ty +mtvu_check dflags ty_fam_ok tv ty = fast_check ty where - details = tcTyVarDetails tv - impredicative_ok = canUnifyWithPolyType dflags details - ok :: MetaTyVarUpdateResult () ok = MTVU_OK () + -- The GHCi runtime debugger does its type-matching with + -- unification variables that can unify with a polytype + -- or a TyCon that would usually be disallowed by bad_tc + -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect + ghci_tv = case tcTyVarDetails tv of + MetaTv { mtv_info = RuntimeUnkTv } -> True + _ -> False + fast_check :: TcType -> MetaTyVarUpdateResult () fast_check (TyVarTy tv') | tv == tv' = MTVU_Occurs @@ -2021,19 +2041,19 @@ preCheck dflags ty_fam_ok tv ty -- in GHC.Core.Type fast_check (TyConApp tc tys) - | bad_tc tc = MTVU_Bad + | bad_tc tc, not ghci_tv = MTVU_Bad | otherwise = mapM fast_check tys >> ok fast_check (LitTy {}) = ok fast_check (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | InvisArg <- af - , not impredicative_ok = MTVU_Bad + , not ghci_tv = MTVU_Bad | otherwise = fast_check w >> fast_check a >> fast_check r fast_check (AppTy fun arg) = fast_check fun >> fast_check arg fast_check (CastTy ty co) = fast_check ty >> fast_check_co co fast_check (CoercionTy co) = fast_check_co co fast_check (ForAllTy (Bndr tv' _) ty) - | not impredicative_ok = MTVU_Bad - | tv == tv' = ok + | not ghci_tv = MTVU_Bad + | tv == tv' = ok | otherwise = do { fast_check_occ (tyVarKind tv') ; fast_check_occ ty } -- Under a forall we look only for occurrences of @@ -2056,14 +2076,6 @@ preCheck dflags ty_fam_ok tv ty bad_tc :: TyCon -> Bool bad_tc tc - | not (impredicative_ok || isTauTyCon tc) = True - | not (ty_fam_ok || isFamFreeTyCon tc) = True - | otherwise = False - -canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool -canUnifyWithPolyType dflags details - = case details of - MetaTv { mtv_info = TyVarTv } -> False - MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags - _other -> True - -- We can have non-meta tyvars in given constraints + | not (isTauTyCon tc) = True + | not (ty_fam_ok || isFamFreeTyCon tc) = True + | otherwise = False diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index a54107fe07..7b4561420c 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -5,14 +5,14 @@ import GHC.Tc.Utils.TcType ( TcTauType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper ) import GHC.Tc.Types.Origin ( CtOrigin ) -import GHC.Hs.Expr ( HsExpr ) -import GHC.Hs.Type ( HsType, Mult ) -import GHC.Hs.Extension ( GhcRn ) +import GHC.Utils.Outputable( SDoc ) +import GHC.Hs.Type ( Mult ) + -- This boot file exists only to tie the knot between -- GHC.Tc.Utils.Unify and Inst -unifyType :: Maybe (HsExpr GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion -unifyKind :: Maybe (HsType GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion +unifyType :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion +unifyKind :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index 296dfa79a4..e00b5a09e3 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -723,6 +723,14 @@ zonkExpr env (HsVar x (L l id)) = ASSERT2( isNothing (isDataConId_maybe id), ppr id ) return (HsVar x (L l (zonkIdOcc env id))) +zonkExpr env (HsUnboundVar v occ) + = return (HsUnboundVar (zonkIdOcc env v) occ) + +zonkExpr env (HsRecFld _ (Ambiguous v occ)) + = return (HsRecFld noExtField (Ambiguous (zonkIdOcc env v) occ)) +zonkExpr env (HsRecFld _ (Unambiguous v occ)) + = return (HsRecFld noExtField (Unambiguous (zonkIdOcc env v) occ)) + zonkExpr _ e@(HsConLikeOut {}) = return e zonkExpr _ (HsIPVar x id) @@ -915,9 +923,6 @@ zonkExpr env (XExpr (WrapExpr (HsWrap co_fn expr))) zonkExpr env (XExpr (ExpansionExpr (HsExpanded a b))) = XExpr . ExpansionExpr . HsExpanded a <$> zonkExpr env b -zonkExpr _ e@(HsUnboundVar {}) - = return e - zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr) ------------------------------------------------------------------------- diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index f89ec4d966..e00b39b20e 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -456,7 +456,7 @@ instance Outputable Rank where rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes") -tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism") +tyConArgMonoType = MonoType (text "Perhaps you intended to use ImpredicativeTypes") synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms") constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype" , text "Perhaps you intended to use QuantifiedConstraints" ]) diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index b58ae7f38e..9665b5e4e2 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -475,6 +475,8 @@ Library GHC.Tc.Deriv.Utils GHC.Tc.Utils.Env GHC.Tc.Gen.Expr + GHC.Tc.Gen.App + GHC.Tc.Gen.Head GHC.Tc.Gen.Foreign GHC.Tc.Deriv.Generate GHC.Tc.Deriv.Functor diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst index bdc0271e6f..516bf36563 100644 --- a/docs/users_guide/9.2.1-notes.rst +++ b/docs/users_guide/9.2.1-notes.rst @@ -3,6 +3,17 @@ Version 9.2.1 ============== +Language +~~~~~~~~ + +* :extension:`ImpredicativeTypes`: Finally, polymorphic types have become first class! + GHC 9.2 includes a full implementation of the Quick Look approach to type inference for + impredicative types, as described in in the paper + `A quick look at impredicativity + <https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__ + (Serrano et al, ICFP 2020). More information here: :ref:`impredicative-polymorphism`. + This replaces the old (undefined, flaky) behaviour of the :extension:`ImpredicativeTypes` extension. + Compiler ~~~~~~~~ diff --git a/docs/users_guide/exts/impredicative_types.rst b/docs/users_guide/exts/impredicative_types.rst index 2380526fb6..01d6476923 100644 --- a/docs/users_guide/exts/impredicative_types.rst +++ b/docs/users_guide/exts/impredicative_types.rst @@ -25,33 +25,32 @@ instantiate ``id``\'s type with ``b := (forall s. ST s a) -> a``, and that is not allowed. Instantiating polymorphic type variables with polymorphic types is called *impredicative polymorphism*. -GHC has extremely flaky support for *impredicative polymorphism*, -enabled with :extension:`ImpredicativeTypes`. If it worked, this would mean -that you *could* call a polymorphic function at a polymorphic type, and -parameterise data structures over polymorphic types. For example: :: - - f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) - f (Just g) = Just (g [3], g "hello") - f Nothing = Nothing - -Notice here that the ``Maybe`` type is parameterised by the -*polymorphic* type ``(forall a. [a] -> [a])``. However *the extension -should be considered highly experimental, and certainly un-supported*. -You are welcome to try it, but please don't rely on it working -consistently, or working the same in subsequent releases. See -:ghc-wiki:`this wiki page <impredicative-polymorphism>` for more details. - -If you want impredicative polymorphism, the main workaround is to use a -newtype wrapper. The ``id runST`` example can be written using this -workaround like this: :: - - runST :: (forall s. ST s a) -> a - id :: forall b. b -> b - - newtype Wrap a = Wrap { unWrap :: (forall s. ST s a) -> a } - - foo :: (forall s. ST s a) -> a - foo = unWrap (id (Wrap runST)) - -- Here id is called at monomorphic type (Wrap a) - - +GHC has robust support for *impredicative polymorphism*, +enabled with :extension:`ImpredicativeTypes`, using the so-called Quick Look +inference algorithm. It is described in the paper +`A quick look at impredicativity +<https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/>`__ +(Serrano et al, ICFP 2020). + +Switching on :extension:`ImpredicativeTypes` + +- Switches on :extension: `RankNTypes` + +- Allows user-written types to have foralls under type constructors, not just under arrows. + For example ``f :: Maybe (forall a. [a] -> [a])`` is a legal type signature. + +- Allows polymorphic types in Visible Type Application + (when :extension: `TypeApplications` is enabled). For example, you + can write ``reverse @(forall b. b->b) xs``. Using VTA with a + polymorphic type argument is useful in cases when Quick Look cannot + infer the correct instantiation. + +- Switches on the Quick Look type inference algorithm, as described + in the paper. This allows the compiler to infer impredicative instantiations of polymorphic + functions in many cases. For example, ``reverse xs`` will typecheck even if ``xs :: [forall a. a->a]``, + by instantiating ``reverse`` at type ``forall a. a->a``. + +For many years GHC has a special case for the function ``($)``, that allows it +to typecheck an application like ``runST $ (do { ... })``, even though that +instantiation may be impredicative. This special case remains: even without +:extension:`ImpredicativeTypes` GHC switches on Quick Look for applications of ``($)``. diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst index d5a2083eab..92dc51e00f 100644 --- a/docs/users_guide/ghci.rst +++ b/docs/users_guide/ghci.rst @@ -2951,37 +2951,20 @@ commonly used commands. .. ghci-cmd:: :type; ⟨expression⟩ - Infers and prints the type of ⟨expression⟩, including explicit - forall quantifiers for polymorphic types. - The type reported is the type that would be inferred - for a variable assigned to the expression, but without the - monomorphism restriction applied. + Infers and prints the type of ⟨expression⟩. For polymorphic types + it instantiates the 'inferred' forall quantifiers (but not the + 'specified' ones; see :ref:`inferred-vs-specified`), solves constraints, and re-generalises. .. code-block:: none *X> :type length length :: Foldable t => t a -> Int -.. ghci-cmd:: :type +v; ⟨expression⟩ - - Infers and prints the type of ⟨expression⟩, but without fiddling - with type variables or class constraints. This is useful when you - are using :extension:`TypeApplications` and care about the distinction - between specified type variables (available for type application) - and inferred type variables (not available). This mode sometimes prints - constraints (such as ``Show Int``) that could readily be solved, but - solving these constraints may affect the type variables, so GHC refrains. - - .. code-block:: none - - *X> :set -fprint-explicit-foralls - *X> :type +v length - length :: forall (t :: * -> *). Foldable t => forall a. t a -> Int - .. ghci-cmd:: :type +d; ⟨expression⟩ - Infers and prints the type of ⟨expression⟩, defaulting type variables - if possible. In this mode, if the inferred type is constrained by + Infers and prints the type of ⟨expression⟩, instantiating *all* the forall + quantifiers, solving constraints, defaulting, and generalising. + In this mode, if the inferred type is constrained by any interactive class (``Num``, ``Show``, ``Eq``, ``Ord``, ``Foldable``, or ``Traversable``), the constrained type variable(s) are defaulted according to the rules described under :extension:`ExtendedDefaultRules`. diff --git a/ghc/GHCi/UI.hs b/ghc/GHCi/UI.hs index 3ccd2e2678..6112428d22 100644 --- a/ghc/GHCi/UI.hs +++ b/ghc/GHCi/UI.hs @@ -2116,13 +2116,16 @@ exceptT = ExceptT . pure -- | @:type@ command. See also Note [TcRnExprMode] in GHC.Tc.Module. typeOfExpr :: GHC.GhcMonad m => String -> m () -typeOfExpr str = handleSourceError GHC.printException $ do - let (mode, expr_str) = case break isSpace str of - ("+d", rest) -> (GHC.TM_Default, dropWhile isSpace rest) - ("+v", rest) -> (GHC.TM_NoInst, dropWhile isSpace rest) - _ -> (GHC.TM_Inst, str) - ty <- GHC.exprType mode expr_str - printForUser $ sep [text expr_str, nest 2 (dcolon <+> pprTypeForUser ty)] +typeOfExpr str = handleSourceError GHC.printException $ + case break isSpace str of + ("+v", _) -> printForUser (text "`:type +v' has gone; use `:type' instead") + ("+d", rest) -> do_it GHC.TM_Default (dropWhile isSpace rest) + _ -> do_it GHC.TM_Inst str + where + do_it mode expr_str + = do { ty <- GHC.exprType mode expr_str + ; printForUser $ sep [ text expr_str + , nest 2 (dcolon <+> pprTypeForUser ty)] } ----------------------------------------------------------------------------- -- | @:type-at@ command diff --git a/testsuite/tests/boxy/Base1.stderr b/testsuite/tests/boxy/Base1.stderr deleted file mode 100644 index e9b2144533..0000000000 --- a/testsuite/tests/boxy/Base1.stderr +++ /dev/null @@ -1,20 +0,0 @@ - -Base1.hs:20:13: error: - • Couldn't match type: a0 -> a0 - with: forall a. a -> a - Expected: MEither Sid b - Actual: MEither (a0 -> a0) b - • In the expression: MLeft fid - In an equation for ‘test1’: test1 fid = MLeft fid - -Base1.hs:25:39: error: - • Couldn't match type: a1 -> a1 - with: forall a. a -> a - Expected: Maybe (Sid, Sid) - Actual: Maybe (a1 -> a1, a2 -> a2) - • In the expression: Just (x, y) - In a case alternative: MRight y -> Just (x, y) - In the expression: - case m of - MRight y -> Just (x, y) - _ -> Nothing diff --git a/testsuite/tests/boxy/Church1.hs b/testsuite/tests/boxy/Church1.hs deleted file mode 100644 index fccaac7d8c..0000000000 --- a/testsuite/tests/boxy/Church1.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# LANGUAGE RankNTypes #-} - -module Church1 where --- Church numerals w/o extra type constructors - -type CNat = forall a. (a->a) -> a -> a - -n0 :: CNat -n0 = \f z -> z - -n1 :: CNat -n1 = \f z -> f z - -nsucc :: CNat -> CNat -nsucc n = \f z -> f (n f z) - -add, mul :: CNat -> CNat -> CNat -add m n = \f -> \a -> m f (n f a) -mul m n = \f -> \a -> m (n f) a - --- already works with GHC 6.4 -exp0 :: CNat -> CNat -> CNat -exp0 m n = n m - - -exp1 :: CNat -> CNat -> CNat -exp1 m n = (n::((CNat -> CNat) -> CNat -> CNat)) (mul m) n1 -- checks with app rule - diff --git a/testsuite/tests/boxy/Church2.hs b/testsuite/tests/boxy/Church2.hs deleted file mode 100644 index c360bb3a8b..0000000000 --- a/testsuite/tests/boxy/Church2.hs +++ /dev/null @@ -1,27 +0,0 @@ -{-# LANGUAGE RankNTypes #-} - -module Church2 where --- Church numerals w/o extra type constructors: Should fail - -type CNat = forall a. (a->a) -> a -> a - -n0 :: CNat -n0 = \f z -> z - -n1 :: CNat -n1 = \f z -> f z - -nsucc :: CNat -> CNat -nsucc n = \f z -> f (n f z) - -add, mul :: CNat -> CNat -> CNat -add m n = \f -> \a -> m f (n f a) -mul m n = \f -> \a -> m (n f) a - --- already works with GHC 6.4 -exp0 :: CNat -> CNat -> CNat -exp0 m n = n m - --- should fail! -exp2 :: CNat -> CNat -> CNat -exp2 m n = n (mul m) n1 diff --git a/testsuite/tests/boxy/Church2.stderr b/testsuite/tests/boxy/Church2.stderr deleted file mode 100644 index ea7613733b..0000000000 --- a/testsuite/tests/boxy/Church2.stderr +++ /dev/null @@ -1,12 +0,0 @@ - -Church2.hs:27:14: - Couldn't match expected type `CNat' - against inferred type `(a -> a) -> a -> a' - In the first argument of `n', namely `(mul m)' - In the expression: n (mul m) n1 - In the definition of `exp2': exp2 m n = n (mul m) n1 - -*** This error message is not helpful, -*** and the test should fail, not pass -*** These comments are here to make sure the output -*** doesn't match! diff --git a/testsuite/tests/boxy/SystemF.hs b/testsuite/tests/boxy/SystemF.hs deleted file mode 100644 index 3f5b4b957a..0000000000 --- a/testsuite/tests/boxy/SystemF.hs +++ /dev/null @@ -1,21 +0,0 @@ -{-# LANGUAGE Rank2Types #-} - -module SystemF where --- System-F examples - - -type Sid = forall a. a -> a - -apply :: forall a b . (a -> b) -> a -> b -apply f g = f g - -hr :: (forall a. a -> a) -> (Int,Bool) -hr f = (f 3,f True) - -test0 = apply hr id -- requires smart-app-arg - -selfApp :: Sid -> Sid -selfApp x = (x::(Sid -> Sid)) x - - - diff --git a/testsuite/tests/boxy/all.T b/testsuite/tests/boxy/all.T deleted file mode 100644 index 99ab5367f2..0000000000 --- a/testsuite/tests/boxy/all.T +++ /dev/null @@ -1,11 +0,0 @@ -# Boxy-type tests - -test('Base1', normal, compile_fail, ['']) -test('Church1', expect_broken(4295), compile, ['']) -test('Church2', expect_broken(1330), compile_fail, ['']) -test('PList1', expect_broken(4295), compile, ['']) -test('PList2', expect_broken(4295), compile, ['']) -test('SystemF', expect_broken(4295), compile, ['']) -test('boxy', expect_broken(4295), compile, ['']) -test('Compose', normal, compile, ['']) -test('T2193', normal, compile_and_run, ['']) diff --git a/testsuite/tests/dependent/ghci/T11549.stdout b/testsuite/tests/dependent/ghci/T11549.stdout index 5e23c0da99..b1edea905d 100644 --- a/testsuite/tests/dependent/ghci/T11549.stdout +++ b/testsuite/tests/dependent/ghci/T11549.stdout @@ -3,17 +3,20 @@ ($) :: (a -> b) -> a -> b -- Defined in ‘GHC.Base’ infixr 0 $ TYPE :: RuntimeRep -> * -error :: [Char] -> a +error :: GHC.Stack.Types.HasCallStack => [Char] -> a error :: GHC.Stack.Types.HasCallStack => [Char] -> a -- Defined in ‘GHC.Err’ -fprint-explicit-runtime-reps -($) :: (a -> b) -> a -> b +($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b ($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b -- Defined in ‘GHC.Base’ infixr 0 $ TYPE :: RuntimeRep -> * -error :: [Char] -> a +error + :: forall (r :: RuntimeRep) (a :: TYPE r). + GHC.Stack.Types.HasCallStack => + [Char] -> a error :: forall (r :: RuntimeRep) (a :: TYPE r). GHC.Stack.Types.HasCallStack => diff --git a/testsuite/tests/dependent/ghci/T11786.script b/testsuite/tests/dependent/ghci/T11786.script index 61e3141843..ada3d7b6ca 100644 --- a/testsuite/tests/dependent/ghci/T11786.script +++ b/testsuite/tests/dependent/ghci/T11786.script @@ -1,11 +1,9 @@ :set -fno-print-explicit-runtime-reps :t ($) :t (($)) -:t +v ($) :i ($) :set -fprint-explicit-runtime-reps :t ($) :t (($)) -:t +v ($) :i ($) diff --git a/testsuite/tests/dependent/ghci/T11786.stdout b/testsuite/tests/dependent/ghci/T11786.stdout index 93616ed750..b43290bd2a 100644 --- a/testsuite/tests/dependent/ghci/T11786.stdout +++ b/testsuite/tests/dependent/ghci/T11786.stdout @@ -1,13 +1,13 @@ ($) :: (a -> b) -> a -> b (($)) :: (a -> b) -> a -> b -($) :: (a -> b) -> a -> b ($) :: (a -> b) -> a -> b -- Defined in ‘GHC.Base’ infixr 0 $ -($) :: (a -> b) -> a -> b -(($)) :: (a -> b) -> a -> b ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b +(($)) + :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r). + (a -> b) -> a -> b ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b diff --git a/testsuite/tests/ghci/scripts/T11376.stdout b/testsuite/tests/ghci/scripts/T11376.stdout index 01e749a22c..3c7674774c 100644 --- a/testsuite/tests/ghci/scripts/T11376.stdout +++ b/testsuite/tests/ghci/scripts/T11376.stdout @@ -1,6 +1,6 @@ -bar @Int :: Int -> b -> Int -bar @Int :: forall {b}. Int -> b -> Int -prox :: forall {k} {a :: k}. Prox @{k} a +bar @Int :: Show Int => Int -> b -> Int +bar @Int :: forall b. Show Int => Int -> b -> Int +prox :: forall {k} (a :: k). Prox @{k} a prox @Int :: Prox @{*} Int -Prox :: forall {k} {a :: k}. Prox @{k} a +Prox :: forall {k} (a :: k). Prox @{k} a Prox @Int :: Prox @{*} Int diff --git a/testsuite/tests/ghci/scripts/T11721.script b/testsuite/tests/ghci/scripts/T11721.script index 11fa313e3c..840f28d613 100644 --- a/testsuite/tests/ghci/scripts/T11721.script +++ b/testsuite/tests/ghci/scripts/T11721.script @@ -2,6 +2,6 @@ :set -fprint-explicit-foralls import Data.Proxy data X a where { MkX :: b -> Proxy a -> X a } -:type +v MkX -:type +v MkX @Int -:type +v MkX @Int @Maybe +:type MkX +:type MkX @Int +:type MkX @Int @Maybe diff --git a/testsuite/tests/ghci/scripts/T11975.script b/testsuite/tests/ghci/scripts/T11975.script index 80061ef97b..72b1a5caff 100644 --- a/testsuite/tests/ghci/scripts/T11975.script +++ b/testsuite/tests/ghci/scripts/T11975.script @@ -1,9 +1,5 @@ :set -fprint-explicit-foralls :type mapM -:type +v mapM -:t +v mapM let foo :: (Show a, Num b) => a -> b; foo = undefined :set -XTypeApplications :type foo @Int -:type +v foo @Int -:t +v foo @Int diff --git a/testsuite/tests/ghci/scripts/T11975.stdout b/testsuite/tests/ghci/scripts/T11975.stdout index 56d8d4180d..86d44bd223 100644 --- a/testsuite/tests/ghci/scripts/T11975.stdout +++ b/testsuite/tests/ghci/scripts/T11975.stdout @@ -1,15 +1,5 @@ mapM - :: forall {t :: * -> *} {m :: * -> *} {a} {b}. - (Traversable t, Monad m) => - (a -> m b) -> t a -> m (t b) -mapM - :: forall (t :: * -> *) (m :: * -> *) a b. - (Traversable t, Monad m) => - (a -> m b) -> t a -> m (t b) -mapM :: forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) -foo @Int :: forall {b}. Num b => Int -> b -foo @Int :: forall b. (Show Int, Num b) => Int -> b foo @Int :: forall b. (Show Int, Num b) => Int -> b diff --git a/testsuite/tests/ghci/scripts/T12550.stdout b/testsuite/tests/ghci/scripts/T12550.stdout index a3117d02c2..fb0bf4c697 100644 --- a/testsuite/tests/ghci/scripts/T12550.stdout +++ b/testsuite/tests/ghci/scripts/T12550.stdout @@ -1,16 +1,16 @@ -f :: forall {a :: * -> *} {b}. C a => a b -f :: forall {a :: * -> *} {b}. C a => a b -f :: forall {a :: * -> *} {b}. C a => a b -f :: forall {a :: * -> *} {b}. C a => a b -f :: forall {a :: * -> *} {b}. C a => a b -f :: forall {a :: * -> *} {b}. C a => a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b -fmap ∷ ∀ {f ∷ ★ → ★} {a} {b}. Functor f ⇒ (a → b) → f a → f b +f :: forall (a :: * -> *) b. C a => a b +f :: forall (a :: * -> *) b. C a => a b +f :: forall (a :: * -> *) b. C a => a b +f :: forall (a :: * -> *) b. C a => a b +f :: forall (a :: * -> *) b. C a => a b +f :: forall (a :: * -> *) b. C a => a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b +fmap ∷ ∀ (f ∷ ★ → ★) a b. Functor f ⇒ (a → b) → f a → f b type Functor :: (★ → ★) → Constraint class Functor f where fmap ∷ ∀ a b. (a → b) → f a → f b @@ -57,7 +57,7 @@ instance ∀ a b c. Functor ((,,,) a b c) -- Defined in ‘GHC.Base’ instance ∀ a b. Functor ((,,) a b) -- Defined in ‘GHC.Base’ instance ∀ a. Functor ((,) a) -- Defined in ‘GHC.Base’ datatypeName - ∷ ∀ {d} {t ∷ ★ → (★ → ★) → ★ → ★} {f ∷ ★ → ★} {a}. + ∷ ∀ d k1 (t ∷ ★ → (k1 → ★) → k1 → ★) (f ∷ k1 → ★) (a ∷ k1). Datatype d ⇒ t d f a → [Char] type Datatype :: ∀ {k}. k → Constraint @@ -67,6 +67,7 @@ class Datatype d where t d f a → [Char] ... -- Defined in ‘GHC.Generics’ -(:*:) ∷ ∀ {f ∷ ★ → ★} {p} {g ∷ ★ → ★}. f p → g p → (:*:) f g p +(:*:) + ∷ ∀ k (f ∷ k → ★) (g ∷ k → ★) (p ∷ k). f p → g p → (:*:) f g p Rep ∷ ★ → ★ → ★ M1 ∷ ∀ k. ★ → Meta → (k → ★) → k → ★ diff --git a/testsuite/tests/ghci/scripts/T13988.script b/testsuite/tests/ghci/scripts/T13988.script index 06aa686ed5..ac18e578be 100644 --- a/testsuite/tests/ghci/scripts/T13988.script +++ b/testsuite/tests/ghci/scripts/T13988.script @@ -1,2 +1,2 @@ :load T13988 -:type +v MkFoo +:type MkFoo diff --git a/testsuite/tests/ghci/scripts/T16804.stdout b/testsuite/tests/ghci/scripts/T16804.stdout index 1c2d73b3c8..1bde0be8e7 100644 --- a/testsuite/tests/ghci/scripts/T16804.stdout +++ b/testsuite/tests/ghci/scripts/T16804.stdout @@ -6,7 +6,7 @@ Collecting type info for 3 module(s) ... % ^~~~~~^ > % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":uses T16804a.hs 1 8 1 14" % file snippet: @@ -22,7 +22,7 @@ undefined :: forall {a}. a % ^~~^ > % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 3 8 3 18 undefined" % file snippet: @@ -31,7 +31,7 @@ undefined :: forall {a}. a % ^~~~~~~~~~^ > % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 3 13 3 18 undefined" % file snippet: @@ -40,7 +40,7 @@ undefined :: forall {a}. a % ^~~~~^ > % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":uses T16804a.hs 3 8 3 11" % file snippet: @@ -73,7 +73,7 @@ undefined :: forall {a}. a % ^~~^ > deriving (Show) % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 5 13 5 13 undefined" % file snippet: @@ -82,7 +82,7 @@ undefined :: forall {a}. a % ^ > deriving (Show) % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 5 15 5 15 undefined" % file snippet: @@ -91,7 +91,7 @@ undefined :: forall {a}. a % ^ > deriving (Show) % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 5 17 5 17 undefined" % file snippet: @@ -100,7 +100,7 @@ undefined :: forall {a}. a % ^ > deriving (Show) % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 6 13 6 16 undefined" % file snippet: @@ -160,7 +160,7 @@ T16804a.hs:(6,13)-(6,16) % ^~~~~^ > mempty = A % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 7 17 7 20 undefined" % file snippet: @@ -169,7 +169,7 @@ undefined :: forall {a}. a % ^~~^ > mempty = A % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 7 10 7 20 undefined" % file snippet: @@ -249,7 +249,7 @@ T16804a.hs:(8,3)-(8,8) % ^~~~~~~~~~~^ > testFunction A B = True % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 13 1 13 12 undefined" % file snippet: @@ -566,7 +566,7 @@ undefined :: Test > B <> _ = B % ^^ % output: -undefined :: forall {a}. a +undefined :: forall a. GHC.Stack.Types.HasCallStack => a % executing: ":type-at T16804a.hs 29 8 29 8 undefined" % file snippet: diff --git a/testsuite/tests/ghci/scripts/T17403.script b/testsuite/tests/ghci/scripts/T17403.script index ad0f9cd83f..624e6a5c2d 100644 --- a/testsuite/tests/ghci/scripts/T17403.script +++ b/testsuite/tests/ghci/scripts/T17403.script @@ -1,2 +1,2 @@ :load T17403 -:type +v f +:type f diff --git a/testsuite/tests/ghci/scripts/T17403.stdout b/testsuite/tests/ghci/scripts/T17403.stdout index c543c3d0e5..deff4906ac 100644 --- a/testsuite/tests/ghci/scripts/T17403.stdout +++ b/testsuite/tests/ghci/scripts/T17403.stdout @@ -1 +1 @@ -f :: (() :: Constraint) => String +f :: String diff --git a/testsuite/tests/ghci/scripts/TypeAppData.stdout b/testsuite/tests/ghci/scripts/TypeAppData.stdout index dd548c85da..19e541d4b4 100644 --- a/testsuite/tests/ghci/scripts/TypeAppData.stdout +++ b/testsuite/tests/ghci/scripts/TypeAppData.stdout @@ -1,13 +1,13 @@ -P1 :: forall {k} {a :: k}. P1 a -P2 :: forall {k} {a :: k}. P2 a -P3 :: forall {k} {a :: k}. P3 k a -P4 :: forall {k} {a :: k}. P1 a -> P4 a -P5 :: forall {k} {a :: k}. P1 a -> P5 -P6 :: forall {k} {a :: k}. P1 a -> P6 -P7 :: forall {k} {a :: k}. P1 a -P8 :: forall {k} {a :: k}. P1 a -P9 :: forall {k} {a :: k}. P1 a -P11 :: forall {k} {a :: k}. P1 a -> P5 -P12 :: forall {k} {a :: k}. P1 a -> P5 -P13 :: forall {k} {a :: k}. P1 a -> P5 -P14 :: forall {k} {a :: k}. P1 a -> P5 +P1 :: forall {k} (a :: k). P1 a +P2 :: forall k (a :: k). P2 a +P3 :: forall k (a :: k). P3 k a +P4 :: forall {k} (a :: k). P1 a -> P4 a +P5 :: forall {k} (a :: k). P1 a -> P5 +P6 :: forall k (a :: k). P1 a -> P6 +P7 :: forall {k} (a :: k). P1 a +P8 :: forall {k} (a :: k). P1 a +P9 :: forall k (a :: k). P1 a +P11 :: forall {k} (a :: k). P1 a -> P5 +P12 :: forall {k} (a :: k). P1 a -> P5 +P13 :: forall k (a :: k). P1 a -> P5 +P14 :: forall k (a :: k). P1 a -> P5 diff --git a/testsuite/tests/ghci/should_run/T12549.stdout b/testsuite/tests/ghci/should_run/T12549.stdout index 8143b156c8..07332c3eca 100644 --- a/testsuite/tests/ghci/should_run/T12549.stdout +++ b/testsuite/tests/ghci/should_run/T12549.stdout @@ -1,3 +1,3 @@ -f :: forall {k1} {k2} {a :: k1 -> k2 -> *} {b :: k1} {c :: k2}. +f :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1) (c :: k2). C a => a b c diff --git a/testsuite/tests/ghci/should_run/T14125a.script b/testsuite/tests/ghci/should_run/T14125a.script index 1667349160..224aa23f73 100644 --- a/testsuite/tests/ghci/should_run/T14125a.script +++ b/testsuite/tests/ghci/should_run/T14125a.script @@ -4,5 +4,4 @@ data instance Foo Int = FooInt Int :kind! Foo Int let f (FooInt i) = i :info f -:type +v f :type f diff --git a/testsuite/tests/ghci/should_run/T14125a.stdout b/testsuite/tests/ghci/should_run/T14125a.stdout index 7b4e85edd3..7946386098 100644 --- a/testsuite/tests/ghci/should_run/T14125a.stdout +++ b/testsuite/tests/ghci/should_run/T14125a.stdout @@ -2,4 +2,3 @@ Foo Int :: * = Foo Int f :: Foo Int -> Int -- Defined at <interactive>:5:5 f :: Foo Int -> Int -f :: Foo Int -> Int diff --git a/testsuite/tests/ghci/should_run/T15806.stderr b/testsuite/tests/ghci/should_run/T15806.stderr index b7e0b4be56..c25e90fe3a 100644 --- a/testsuite/tests/ghci/should_run/T15806.stderr +++ b/testsuite/tests/ghci/should_run/T15806.stderr @@ -1,3 +1,4 @@ + <interactive>:1:1: error: Illegal polymorphic type: forall a. a -> a - GHC doesn't yet support impredicative polymorphism
\ No newline at end of file + Perhaps you intended to use ImpredicativeTypes diff --git a/testsuite/tests/boxy/Base1.hs b/testsuite/tests/impredicative/Base1.hs index 7e33069199..5e3b377ee2 100644 --- a/testsuite/tests/boxy/Base1.hs +++ b/testsuite/tests/impredicative/Base1.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-} +{-# LANGUAGE ImpredicativeTypes #-} -- Sept 16: now failing, because I've further reduced the scop -- of impredicative types diff --git a/testsuite/tests/impredicative/Church1.hs b/testsuite/tests/impredicative/Church1.hs new file mode 100644 index 0000000000..e5af210385 --- /dev/null +++ b/testsuite/tests/impredicative/Church1.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE ImpredicativeTypes, RankNTypes, ScopedTypeVariables, TypeApplications #-} + +module Church1 where +-- Church numerals w/o extra type constructors + +type CNat = forall a. (a->a) -> a -> a + +n0 :: CNat +n0 = \f z -> z + +n1 :: CNat +n1 = \f z -> f z + +nsucc :: CNat -> CNat +nsucc n = \f z -> f (n f z) + +add, mul :: CNat -> CNat -> CNat +add m n = \f -> \a -> m f (n f a) +mul m n = \f -> \a -> m (n f) a + +-- already works with GHC 6.4 +exp0 :: CNat -> CNat -> CNat +exp0 m n = n m + +exp1 :: CNat -> CNat -> CNat +exp1 m n = n (mul m) n1 + +foldNat :: CNat -> (a -> a) -> a -> a +foldNat n = n + +idC :: CNat -> CNat +idC x = foldNat @CNat x (\y -> nsucc y) n0 + +inc :: CNat -> CNat +inc x = foldNat x nsucc n1 diff --git a/testsuite/tests/boxy/Compose.hs b/testsuite/tests/impredicative/Compose.hs index f3d3a10b28..f3d3a10b28 100644 --- a/testsuite/tests/boxy/Compose.hs +++ b/testsuite/tests/impredicative/Compose.hs diff --git a/testsuite/tests/boxy/Makefile b/testsuite/tests/impredicative/Makefile index 9a36a1c5fe..9a36a1c5fe 100644 --- a/testsuite/tests/boxy/Makefile +++ b/testsuite/tests/impredicative/Makefile diff --git a/testsuite/tests/boxy/PList1.hs b/testsuite/tests/impredicative/PList1.hs index 6869d904cc..27cedc1f49 100644 --- a/testsuite/tests/boxy/PList1.hs +++ b/testsuite/tests/impredicative/PList1.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-} +{-# LANGUAGE ImpredicativeTypes #-} module PList1 where -- Polymorphic lists 1: requires smart-app-res diff --git a/testsuite/tests/boxy/PList2.hs b/testsuite/tests/impredicative/PList2.hs index 316e8792ae..316e8792ae 100644 --- a/testsuite/tests/boxy/PList2.hs +++ b/testsuite/tests/impredicative/PList2.hs diff --git a/testsuite/tests/impredicative/SystemF.hs b/testsuite/tests/impredicative/SystemF.hs new file mode 100644 index 0000000000..b1f7f0ede9 --- /dev/null +++ b/testsuite/tests/impredicative/SystemF.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE ImpredicativeTypes #-} + +module SystemF where +-- System-F examples + + +type Sid = forall a. a -> a + +apply :: forall a b . (a -> b) -> a -> b +apply f g = f g + +hr :: (forall a. a -> a) -> (Int,Bool) +hr f = (f 3,f True) + +test0 = apply hr id -- requires smart-app-arg + +selfApp :: Sid -> Sid +selfApp x = (x::(Sid -> Sid)) x diff --git a/testsuite/tests/impredicative/T17332.hs b/testsuite/tests/impredicative/T17332.hs new file mode 100644 index 0000000000..7b83651740 --- /dev/null +++ b/testsuite/tests/impredicative/T17332.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImpredicativeTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} +module Bug where + +import GHC.Exts + +data Dict c where + MkDict :: c => Dict c + +aux :: Dict (forall a. a) +aux = MkDict + +{- +[W] forall (c:: Constraint). c +==> + forall c. [W] c +-} diff --git a/testsuite/tests/impredicative/T17332.stderr b/testsuite/tests/impredicative/T17332.stderr new file mode 100644 index 0000000000..24bb0e2aee --- /dev/null +++ b/testsuite/tests/impredicative/T17332.stderr @@ -0,0 +1,5 @@ + +T17332.hs:13:7: error: + • Could not deduce: a arising from a use of ‘MkDict’ + • In the expression: MkDict + In an equation for ‘aux’: aux = MkDict diff --git a/testsuite/tests/impredicative/T17372.hs b/testsuite/tests/impredicative/T17372.hs new file mode 100644 index 0000000000..c8a79f3a9e --- /dev/null +++ b/testsuite/tests/impredicative/T17372.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE ImpredicativeTypes, ConstraintKinds, GADTs, AllowAmbiguousTypes #-} + +module T17372 where + +-- This typechecks +x1 = () :: ((Show a => Num a => Int) ~ ((Show a, Num a) => Int)) => () + +-- -> replace `Num a` with `(Eq a, Ord a)` + +-- This doesn't typecheck +-- Couldn't match type ‘Ord a0 => Int’ with ‘Int’ +x2 = () :: ((Show a => (Eq a, Ord a) => Int) ~ ((Show a, (Eq a, Ord a)) => Int)) => () + +type A a = (Eq a, Ord a) + +-- This typechecks +x3 = () :: (Eq a, Ord a) ~ A a => () + +-- This doesn't typecheck +-- Couldn't match type ‘()’ with ‘Ord a0 -> ()’ +x4 = () :: (A a => ()) ~ ((Eq a, Ord a) => ()) => () + +-- -> replace `Num a` with `A a` instead + +-- This typechecks +x5 = () :: ((Show a => A a => Int) ~ ((Show a, A a) => Int)) => () + +-- Let's make a type synonym out of the entire constraint +type C c a = ((Show a => c => Int) ~ ((Show a, c) => Int)) + +-- Now all of these typecheck: +x6 = () :: C (Num a) a => () +x7 = () :: C (Eq a, Ord a) a => () +x8 = () :: C (A a) a => () + +-- This doesn't typecheck +x9 = () :: ((() => () => Int) ~ (((), ()) => Int)) => () + +-- Let's turn this constraint into a different type synonym +type B a b = ((a => b => Int) ~ ((a, b) => Int)) + +-- These both typecheck now: +x10 = () :: B (Show a) (Num a) => () +x11 = () :: B () () => () diff --git a/testsuite/tests/impredicative/T18126-1.hs b/testsuite/tests/impredicative/T18126-1.hs new file mode 100644 index 0000000000..bbc3a6ec40 --- /dev/null +++ b/testsuite/tests/impredicative/T18126-1.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE ImplicitParams, TypeApplications, ScopedTypeVariables, QuantifiedConstraints, ImpredicativeTypes #-} + +module Foo where + +import Control.Monad +import GHC.Stack + +wcs :: (?callStack :: CallStack) => ( (?callStack :: CallStack) => a ) -> a +wcs x = error "urk" + +info :: IO () +info = wcs $ (when True $ return ()) diff --git a/testsuite/tests/impredicative/T18126-nasty.hs b/testsuite/tests/impredicative/T18126-nasty.hs new file mode 100644 index 0000000000..0169a59baf --- /dev/null +++ b/testsuite/tests/impredicative/T18126-nasty.hs @@ -0,0 +1,61 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeApplications #-} + +module Bug where + + +-- This nasty example fails with quick-look +-- (which here is switched on by ($)) +-- beecause of a very subtle issue where we instantiate an +-- instantiation variable with (F alpha), where F is a type function +-- +-- It's a stripped-down version of T5490 + +register :: forall rs op_ty. + (HDrop rs ~ HSingle (WaitOpResult op_ty)) + => rs -> op_ty + -> Maybe (WaitOpResult (WaitOps rs)) + -> Int +register _ _ ev + = ($) -- (px -> qx) -> px -> qx px=a_a2iT qx=b_a2iU + (foo ev) -- Instantiate at ax=a2iW bx=a2iX; + -- (ax,bx) -> Int + -- ql on arg ev bx := WaitOpResult (WaitOps rs) = [rs] + -- px := (ax,bx) + -- qx := Int + (inj 3) -- instantiate lx=l_a2iZ; + -- res_ty (HNth n lx, [lx]) + -- res_ty px = (ax,bx) ~ (HNth n lx, [lx]) + -- ax := HNth n lx + -- bx := [lx] + -- Result ql: WaitOpResult op_ty ~ ax = HNth n lx + +{- + ($) @(HNth l0, WR (WO rs)) + @Int + (foo ev) + (inj 3) +-} + + +foo :: forall a b . Maybe b -> (a,b) -> Int +foo = error "urk" + +inj :: Int -> (HNth l, [l]) +inj = error "urk" + +data HSingle a +type family HHead l +type instance HHead (HSingle h) = h + +data WaitOps rs +type family WaitOpResult op +type instance WaitOpResult (WaitOps rs) = [rs] + +type family HDrop l + +type HNth l = HHead (HDrop l) + + + diff --git a/testsuite/tests/boxy/T2193.hs b/testsuite/tests/impredicative/T2193.hs index c36503eae7..dee542c65c 100644 --- a/testsuite/tests/boxy/T2193.hs +++ b/testsuite/tests/impredicative/T2193.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-} +{-# LANGUAGE ImpredicativeTypes #-} -- Sept 16: now scraping through with -XImpredicateTypes diff --git a/testsuite/tests/boxy/T2193.stdout b/testsuite/tests/impredicative/T2193.stdout index b8626c4cff..b8626c4cff 100644 --- a/testsuite/tests/boxy/T2193.stdout +++ b/testsuite/tests/impredicative/T2193.stdout diff --git a/testsuite/tests/impredicative/T7026.hs b/testsuite/tests/impredicative/T7026.hs new file mode 100644 index 0000000000..3ef6ae277b --- /dev/null +++ b/testsuite/tests/impredicative/T7026.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-} + +module Bug where + + f1 :: Maybe ((?a :: Bool) => Char) + f1 = Just 'C' + + f2 :: Maybe ((?a :: Bool) => Bool) + f2 = Just ?a diff --git a/testsuite/tests/impredicative/T8808.hs b/testsuite/tests/impredicative/T8808.hs new file mode 100644 index 0000000000..8b33064a15 --- /dev/null +++ b/testsuite/tests/impredicative/T8808.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-} + +module Test where + +f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) +f1 (Just g) = Just (g [3], g "hello") +f1 Nothing = Nothing + +f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char]) +f2 [g] = Just (g [3], g "hello") +f2 [] = Nothing + +g1 = (f1 . Just) reverse + +g1' = f1 (Just reverse) + +g2 = f2 [reverse] + +-- Left sections not working yet +-- g2' = f2 ((: []) reverse) + +g2'' = f2 (reverse : []) diff --git a/testsuite/tests/impredicative/T9730.hs b/testsuite/tests/impredicative/T9730.hs new file mode 100644 index 0000000000..7a05cb8e63 --- /dev/null +++ b/testsuite/tests/impredicative/T9730.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE ImpredicativeTypes, RankNTypes #-} + +module T9730 where + +class A a where + +class B b where + +class C c where +a2b :: (forall a. A a => a) -> (forall b. B b => b) +a2b = undefined + +b2c :: (forall b. B b => b) -> (forall c. C c => c) +b2c = undefined + +a2c :: (forall a. A a => a) -> (forall c. C c => c) +a2c = b2c . a2b diff --git a/testsuite/tests/impredicative/all.T b/testsuite/tests/impredicative/all.T new file mode 100644 index 0000000000..2f23210f6b --- /dev/null +++ b/testsuite/tests/impredicative/all.T @@ -0,0 +1,22 @@ +# Impredicativity tests + +test('Church2', expect_broken(1330), compile_fail, ['']) + +test('PList1', normal, compile, ['']) +test('PList2', normal, compile, ['']) +test('SystemF', normal, compile, ['']) +test('Base1', normal, compile, ['']) +test('Church1', normal, compile, ['']) +test('boxy', normal, compile, ['']) +test('Compose', normal, compile, ['']) +test('T2193', normal, compile_and_run, ['']) +test('icfp20-ok', normal, compile, ['']) +test('icfp20-fail', normal, compile_fail, ['']) +test('T18126-1', normal, compile, ['']) +test('T18126-nasty', normal, compile, ['']) +test('cabal-example', normal, compile, ['']) +test('T9730', normal, compile, ['']) +test('T7026', normal, compile, ['']) +test('T8808', normal, compile, ['']) +test('T17332', normal, compile_fail, ['']) +test('expr-sig', normal, compile, ['']) diff --git a/testsuite/tests/boxy/boxy.hs b/testsuite/tests/impredicative/boxy.hs index c4835b1c62..475b5c1c5e 100644 --- a/testsuite/tests/boxy/boxy.hs +++ b/testsuite/tests/impredicative/boxy.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables #-} +{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-} module ShouldCompile where @@ -17,7 +17,6 @@ sing x = [x] id1 :: forall a. a -> a id1 = id -{- ids :: [forall a. a -> a] ids = [id1,id1] @@ -29,7 +28,6 @@ t2 = sing id t3 :: forall a. a -> a t3 = head ids --} {--------------- Examples from QMLF paper -------------------} @@ -45,13 +43,11 @@ qH choose id = choose id choose :: forall a. a -> a -> a choose x y = x -{- impred1 :: (Bool, Char) -impred1 = qF $ choose --- impredicative instantiation for $ +impred1 = ($) qF choose --- impredicative instantiation for $ impred2 :: (forall a. a -> a -> a) -> (Bool, Char) impred2 = id qF --} {------ Examples for Garrique/Remy paper -------} @@ -69,33 +65,6 @@ gr2 = self2 id gr3 = (\(u :: (forall a. a -> a) -> (forall a. a -> a)) -> u id) self1 -{------------ Church numerals ----------} - -type Church = forall a. a -> (a -> a) -> a - -z :: Church -z = \z -> \f -> z - -s :: Church -> Church -s = \n -> \z -> \f -> f (n z f) - -fold :: Church -> a -> (a -> a) -> a -fold n f z = n f z - -{- -mul :: Church -> Church -> Church -mul m n = \f -> \a -> m (n f) a - -exp :: Church -> Church -> Church -exp m n = n (mul m) (s z) - -idC :: Church -> Church -idC x = fold x s z - -inc :: Church -> Church -inc x = fold x s (s z) --} - {------- fix for higher rank types ---------} data Tree a = Branch a (Tree (a,a)) | Leaf diff --git a/testsuite/tests/impredicative/cabal-example.hs b/testsuite/tests/impredicative/cabal-example.hs new file mode 100644 index 0000000000..1da77bf0dd --- /dev/null +++ b/testsuite/tests/impredicative/cabal-example.hs @@ -0,0 +1,47 @@ +{- This example illustrates a nasty case of "vacuous" abstraction + It comes from Cabal library Distribution.Simple.Utils + +Consider this + + type HCS = (?callStack :: CallStack) + wcs :: forall a. (HCS => a) -> a + foo :: Int + ($) :: forall p q. (p->q) -> p -> q + +The call: wcs $ foo + +From QL on the first arg of $ we instantiate wcs with a:=kappa. Then +we can work out what p and q must instantiate to. (the (p->q) arg of +($) is guarded): get p := (HCS => kappa), q := kappa + +But alas, the second arg of $, namely foo, satisfies our +fiv(rho_r)=empty condition. (Here rho_r is Int.) So we try to mgu( +HCS => kappa, Int ), and fail. + +The basic problem is this: we said in 5.4 of the Quick Look paper we +didn’t about vacuous type abstraction, but we clearly do care about +type-class abstraction. + +How does this work in GHC today, with the built-in rule? It works +because we are order-dependent: we look at the first argument first. + +The same would work here. If we applied the QL substitution as we go, +by the time we got to the second argument, the expected type would +look like (HCS => kappa), and we would abandon QL on it (App-lightning +only applies to rho). But the price is order-dependence. +-} + +module CabalEx where + +import GHC.Stack( withFrozenCallStack ) + +-- withFrozenCallStack :: HasCallStack +-- => ( HasCallStack => a ) +-- -> a + +printRawCommandAndArgsAndEnv :: Int -> IO () +printRawCommandAndArgsAndEnv = error "urk" + +printRawCommandAndArgs :: Int -> IO () +printRawCommandAndArgs verbosity + = withFrozenCallStack $ printRawCommandAndArgsAndEnv verbosity diff --git a/testsuite/tests/impredicative/expr-sig.hs b/testsuite/tests/impredicative/expr-sig.hs new file mode 100644 index 0000000000..7e155ad600 --- /dev/null +++ b/testsuite/tests/impredicative/expr-sig.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE ImpredicativeTypes, RankNTypes #-} + +module ExprSig where + +import Data.Kind + +f :: [forall a. a->a] -> Int +f x = error "urk" + +g1 = f undefined + +-- This should be accepted (and wasn't) +g2 = f (undefined :: forall b. b) + +f3 :: [forall a. a->a] -> b +f3 x = error "urk" + +g3 = f3 (undefined :: forall b. b) + diff --git a/testsuite/tests/impredicative/icfp20-fail.hs b/testsuite/tests/impredicative/icfp20-fail.hs new file mode 100644 index 0000000000..2e077d7ec1 --- /dev/null +++ b/testsuite/tests/impredicative/icfp20-fail.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE ScopedTypeVariables, TypeApplications, RankNTypes, ImpredicativeTypes #-} + +module ICFP20 where + +import Control.Monad.ST( ST, runST ) + +type SId = forall a. a->a + +choose :: a -> a -> a +choose x y = x + +single :: a -> [a] +single x = [x] + +auto'2 :: SId -> b -> b +auto'2 x = id @SId x + +-- Fails, and should fail +auto'1 :: SId -> b -> b +auto'1 = id + +-- Fails, and should do so +a6 = id auto'2 + +-- Fails, and should do so +a8 = choose id auto'2 + +-- Fails, and should do so +st2 :: forall a. (forall s. ST s a) -> a +st2 x = id runST x diff --git a/testsuite/tests/impredicative/icfp20-fail.stderr b/testsuite/tests/impredicative/icfp20-fail.stderr new file mode 100644 index 0000000000..c9e06b10cc --- /dev/null +++ b/testsuite/tests/impredicative/icfp20-fail.stderr @@ -0,0 +1,42 @@ + +icfp20-fail.hs:20:10: error: + • Couldn't match type: forall a. a -> a + with: b -> b + Expected: SId -> b -> b + Actual: SId -> SId + • In the expression: id + In an equation for ‘auto'1’: auto'1 = id + • Relevant bindings include + auto'1 :: SId -> b -> b (bound at icfp20-fail.hs:20:1) + +icfp20-fail.hs:23:9: error: + • Couldn't match expected type ‘a0’ + with actual type ‘SId -> b0 -> b0’ + Cannot instantiate unification variable ‘a0’ + with a type involving polytypes: SId -> b0 -> b0 + • In the first argument of ‘id’, namely ‘auto'2’ + In the expression: id auto'2 + In an equation for ‘a6’: a6 = id auto'2 + • Relevant bindings include a6 :: a0 (bound at icfp20-fail.hs:23:1) + +icfp20-fail.hs:26:16: error: + • Couldn't match type ‘SId’ with ‘b -> b’ + Expected: (b -> b) -> b -> b + Actual: SId -> b -> b + • In the second argument of ‘choose’, namely ‘auto'2’ + In the expression: choose id auto'2 + In an equation for ‘a8’: a8 = choose id auto'2 + • Relevant bindings include + a8 :: (b -> b) -> b -> b (bound at icfp20-fail.hs:26:1) + +icfp20-fail.hs:30:12: error: + • Couldn't match type: forall s. ST s a + with: ST s0 a + Expected: ST s0 a -> a + Actual: (forall s. ST s a) -> a + • In the first argument of ‘id’, namely ‘runST’ + In the expression: id runST x + In an equation for ‘st2’: st2 x = id runST x + • Relevant bindings include + x :: forall s. ST s a (bound at icfp20-fail.hs:30:5) + st2 :: (forall s. ST s a) -> a (bound at icfp20-fail.hs:30:1) diff --git a/testsuite/tests/impredicative/icfp20-ok.hs b/testsuite/tests/impredicative/icfp20-ok.hs new file mode 100644 index 0000000000..c5b5e6acfc --- /dev/null +++ b/testsuite/tests/impredicative/icfp20-ok.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE ScopedTypeVariables, TypeApplications, RankNTypes, ImpredicativeTypes #-} + +module ICFP20 where + +import Control.Monad.ST( ST, runST ) + +type SId = forall a. a->a + +ids :: [SId] +ids = [id,id] + +choose :: a -> a -> a +choose x y = x + +auto :: SId -> SId +auto = id + +single :: a -> [a] +single x = [x] + +auto'2 :: SId -> b -> b +auto'2 x = id @SId x + +auto3 :: SId -> b -> b +auto3 x = id x + +poly :: SId -> (Int,Bool) +poly f = (f (3::Int), f True) + +f :: (a->a) -> [a] -> a +f g xs = g (head xs) + +inc :: Int -> Int +inc x = x+1 + +app :: (a->b) -> a -> b +app f x = f x + +revapp :: a -> (a->b) -> b +revapp x f = f x + +a3 = choose [] ids +a5 = id auto +a7 = choose id auto +a9 = f (choose id) ids +a10 = poly id +a11 = poly (\x -> x) +a12 = id poly (\x -> x) + +c1 = length ids +c2 = tail ids +c3 = head ids +c4 = single id :: [SId] +c5 = id : ids +c6 = id : id : ids +c7 = single inc ++ single id +c8a = ids ++ single id +c8b = single id ++ ids +c9 = map poly (single id) + +argST :: forall s. ST s Int +argST = error "urk" + +d1a = poly $ id +d1b = app poly id +d2 = revapp id poly +d3 = runST argST +d4 = runST $ argST + +st1 :: forall a. (forall s. ST s a) -> a +st1 x = id (runST @a) x + +-- Not in the paper's table +c10 = head ids True diff --git a/testsuite/tests/linear/should_run/LinearGhci.script b/testsuite/tests/linear/should_run/LinearGhci.script index 78f81ef8d2..cd55fe73bd 100644 --- a/testsuite/tests/linear/should_run/LinearGhci.script +++ b/testsuite/tests/linear/should_run/LinearGhci.script @@ -1,11 +1,11 @@ data T a = MkT a -:type +v MkT +:type MkT :set -XLinearTypes -:type +v MkT +:type MkT :set -XGADTs data T a where MkT :: a #-> a -> T a :info T data T a b m n r = MkT a b m n r :set -fprint-explicit-foralls -- check that user variables are not renamed (see dataConMulVars) -:type +v MkT +:type MkT diff --git a/testsuite/tests/polykinds/KindVarOrder.script b/testsuite/tests/polykinds/KindVarOrder.script index c4b4165dcf..945313a6e3 100644 --- a/testsuite/tests/polykinds/KindVarOrder.script +++ b/testsuite/tests/polykinds/KindVarOrder.script @@ -4,6 +4,6 @@ data Proxy (a :: k) f :: Proxy (a :: k) -> Proxy (b :: j) -> (); f = f g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> (); g = g h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> (); h = h -:t +v f -:t +v g -:t +v h +:t f +:t g +:t h diff --git a/testsuite/tests/typecheck/should_fail/T11355.stderr b/testsuite/tests/typecheck/should_fail/T11355.stderr index 5310989327..c922e4db93 100644 --- a/testsuite/tests/typecheck/should_fail/T11355.stderr +++ b/testsuite/tests/typecheck/should_fail/T11355.stderr @@ -1,7 +1,7 @@ T11355.hs:5:7: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism + Perhaps you intended to use ImpredicativeTypes • In the expression: const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a)) In an equation for ‘foo’: diff --git a/testsuite/tests/typecheck/should_fail/T2538.stderr b/testsuite/tests/typecheck/should_fail/T2538.stderr index 18c82bd992..726ac8fd71 100644 --- a/testsuite/tests/typecheck/should_fail/T2538.stderr +++ b/testsuite/tests/typecheck/should_fail/T2538.stderr @@ -2,17 +2,14 @@ T2538.hs:6:6: error: • Illegal qualified type: Eq a => a -> a Perhaps you intended to use RankNTypes - • In the type signature: - f :: (Eq a => a -> a) -> Int + • In the type signature: f :: (Eq a => a -> a) -> Int T2538.hs:9:6: error: • Illegal qualified type: Eq a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - g :: [Eq a => a -> a] -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: g :: [Eq a => a -> a] -> Int T2538.hs:12:6: error: • Illegal qualified type: Eq a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - h :: Ix (Eq a => a -> a) => Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: h :: Ix (Eq a => a -> a) => Int diff --git a/testsuite/tests/typecheck/should_fail/T7809.stderr b/testsuite/tests/typecheck/should_fail/T7809.stderr index 9ec32b3ff6..0e0c867659 100644 --- a/testsuite/tests/typecheck/should_fail/T7809.stderr +++ b/testsuite/tests/typecheck/should_fail/T7809.stderr @@ -1,6 +1,6 @@ T7809.hs:8:8: error: • Illegal polymorphic type: forall a. a -> a - GHC doesn't yet support impredicative polymorphism + Perhaps you intended to use ImpredicativeTypes • In the expansion of type synonym ‘PolyId’ In the type signature: foo :: F PolyId diff --git a/testsuite/tests/typecheck/should_fail/tcfail127.stderr b/testsuite/tests/typecheck/should_fail/tcfail127.stderr index 6716724860..a262e0113e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail127.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail127.stderr @@ -1,6 +1,5 @@ tcfail127.hs:3:8: error: • Illegal qualified type: Num a => a -> a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - foo :: IO (Num a => a -> a) + Perhaps you intended to use ImpredicativeTypes + • In the type signature: foo :: IO (Num a => a -> a) diff --git a/testsuite/tests/typecheck/should_fail/tcfail196.stderr b/testsuite/tests/typecheck/should_fail/tcfail196.stderr index 57370d4014..313e7cbdd4 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail196.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail196.stderr @@ -1,6 +1,5 @@ tcfail196.hs:5:8: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - bar :: Num (forall a. a) => Int -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: bar :: Num (forall a. a) => Int -> Int diff --git a/testsuite/tests/typecheck/should_fail/tcfail197.stderr b/testsuite/tests/typecheck/should_fail/tcfail197.stderr index 1d5f455968..cfbc3fd0dd 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail197.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail197.stderr @@ -1,6 +1,5 @@ tcfail197.hs:5:8: error: • Illegal polymorphic type: forall a. a - GHC doesn't yet support impredicative polymorphism - • In the type signature: - foo :: [forall a. a] -> Int + Perhaps you intended to use ImpredicativeTypes + • In the type signature: foo :: [forall a. a] -> Int diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T index f69cc71352..ef8ae9136d 100755 --- a/testsuite/tests/typecheck/should_run/all.T +++ b/testsuite/tests/typecheck/should_run/all.T @@ -58,7 +58,7 @@ test('tcrun038', [extra_files(['TcRun038_B.hs'])], multimod_compile_and_run, ['t test('tcrun039', normal, compile_and_run, ['']) test('tcrun040', normal, compile_and_run, ['']) test('tcrun041', omit_ways(['ghci']), compile_and_run, ['']) -test('tcrun042', normal, compile, ['']) +test('tcrun042', normal, compile_fail, ['']) test('tcrun043', normal, compile_and_run, ['']) test('tcrun044', normal, compile_and_run, ['']) test('tcrun045', normal, compile_fail, ['']) @@ -96,7 +96,7 @@ test('T6117', normal, compile_and_run, ['']) test('T5751', normal, compile_and_run, ['']) test('T5913', normal, compile_and_run, ['']) test('T7748', normal, compile_and_run, ['']) -test('T7861', [omit_ways(['debug']), exit_code(1)], compile_and_run, ['']) +test('T7861', [expect_broken(18467),omit_ways(['debug']), exit_code(1)], compile_and_run, ['']) test('TcTypeNatSimpleRun', normal, compile_and_run, ['']) test('TcTypeSymbolSimpleRun', normal, compile_and_run, ['']) test('T8119', normal, ghci_script, ['T8119.script']) diff --git a/testsuite/tests/typecheck/should_run/tcrun042.hs b/testsuite/tests/typecheck/should_run/tcrun042.hs index ba809a16ba..30c67601ed 100644 --- a/testsuite/tests/typecheck/should_run/tcrun042.hs +++ b/testsuite/tests/typecheck/should_run/tcrun042.hs @@ -7,6 +7,11 @@ -- -- Apr 20: Works again. NB: the ImpredicativeTypes flag -- +-- July 20: Fails again. Under Quick Look this now fails, because +-- we don't have a special typing rule for ExplicitTuples +-- We could, and it would improve the typing for tuple sections. +-- But for now I'm just letting it fail, until someone yells. +-- -- The test was added by Max in 5e8ff849, apparently to test tuple sections module Main where diff --git a/testsuite/tests/typecheck/should_run/tcrun042.stderr b/testsuite/tests/typecheck/should_run/tcrun042.stderr new file mode 100644 index 0000000000..dcf0854d47 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/tcrun042.stderr @@ -0,0 +1,10 @@ + +tcrun042.hs:20:5: error: + • Couldn't match type ‘t0’ with ‘forall b. b -> b -> b’ + Expected: a + -> (forall b. b -> b -> b) -> (a, String, forall c. c -> c -> c) + Actual: a -> t0 -> (a, [Char], t0) + Cannot instantiate unification variable ‘t0’ + with a type involving polytypes: forall b. b -> b -> b + • In the expression: (, "Hello" ++ "World",) + In an equation for ‘e’: e = (, "Hello" ++ "World",) diff --git a/utils/haddock b/utils/haddock -Subproject 2a15172bde75ec151a52fef586d1e362d478aae +Subproject 8c8517d6c82411212452c3c5fca503c7af5ac3d |