diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-02-02 18:23:11 +0000 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2020-06-05 09:27:50 -0400 |
| commit | 2b792facab46f7cdd09d12e79499f4e0dcd4293f (patch) | |
| tree | f3bf2dffdd3c46744d3c1b0638948a1dfbd1b8f6 /compiler | |
| parent | af5e3a885ddd09dd5f550552c535af3661ff3dbf (diff) | |
| download | haskell-2b792facab46f7cdd09d12e79499f4e0dcd4293f.tar.gz | |
Simple subsumptionwip/T17775
This patch simplifies GHC to use simple subsumption.
Ticket #17775
Implements GHC proposal #287
https://github.com/ghc-proposals/ghc-proposals/blob/master/
proposals/0287-simplify-subsumption.rst
All the motivation is described there; I will not repeat it here.
The implementation payload:
* tcSubType and friends become noticably simpler, because it no
longer uses eta-expansion when checking subsumption.
* No deeplyInstantiate or deeplySkolemise
That in turn means that some tests fail, by design; they can all
be fixed by eta expansion. There is a list of such changes below.
Implementing the patch led me into a variety of sticky corners, so
the patch includes several othe changes, some quite significant:
* I made String wired-in, so that
"foo" :: String rather than
"foo" :: [Char]
This improves error messages, and fixes #15679
* The pattern match checker relies on knowing about in-scope equality
constraints, andd adds them to the desugarer's environment using
addTyCsDs. But the co_fn in a FunBind was missed, and for some reason
simple-subsumption ends up with dictionaries there. So I added a
call to addTyCsDs. This is really part of #18049.
* I moved the ic_telescope field out of Implication and into
ForAllSkol instead. This is a nice win; just expresses the code
much better.
* There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader.
We called checkDataKindSig inside tc_kind_sig, /before/
solveEqualities and zonking. Obviously wrong, easily fixed.
* solveLocalEqualitiesX: there was a whole mess in here, around
failing fast enough. I discovered a bad latent bug where we
could successfully kind-check a type signature, and use it,
but have unsolved constraints that could fill in coercion
holes in that signature -- aargh.
It's all explained in Note [Failure in local type signatures]
in GHC.Tc.Solver. Much better now.
* I fixed a serious bug in anonymous type holes. IN
f :: Int -> (forall a. a -> _) -> Int
that "_" should be a unification variable at the /outer/
level; it cannot be instantiated to 'a'. This was plain
wrong. New fields mode_lvl and mode_holes in TcTyMode,
and auxiliary data type GHC.Tc.Gen.HsType.HoleMode.
This fixes #16292, but makes no progress towards the more
ambitious #16082
* I got sucked into an enormous refactoring of the reporting of
equality errors in GHC.Tc.Errors, especially in
mkEqErr1
mkTyVarEqErr
misMatchMsg
misMatchMsgOrCND
In particular, the very tricky mkExpectedActualMsg function
is gone.
It took me a full day. But the result is far easier to understand.
(Still not easy!) This led to various minor improvements in error
output, and an enormous number of test-case error wibbles.
One particular point: for occurs-check errors I now just say
Can't match 'a' against '[a]'
rather than using the intimidating language of "occurs check".
* Pretty-printing AbsBinds
Tests review
* Eta expansions
T11305: one eta expansion
T12082: one eta expansion (undefined)
T13585a: one eta expansion
T3102: one eta expansion
T3692: two eta expansions (tricky)
T2239: two eta expansions
T16473: one eta
determ004: two eta expansions (undefined)
annfail06: two eta (undefined)
T17923: four eta expansions (a strange program indeed!)
tcrun035: one eta expansion
* Ambiguity check at higher rank. Now that we have simple
subsumption, a type like
f :: (forall a. Eq a => Int) -> Int
is no longer ambiguous, because we could write
g :: (forall a. Eq a => Int) -> Int
g = f
and it'd typecheck just fine. But f's type is a bit
suspicious, and we might want to consider making the
ambiguity check do a check on each sub-term. Meanwhile,
these tests are accepted, whereas they were previously
rejected as ambiguous:
T7220a
T15438
T10503
T9222
* Some more interesting error message wibbles
T13381: Fine: one error (Int ~ Exp Int)
rather than two (Int ~ Exp Int, Exp Int ~ Int)
T9834: Small change in error (improvement)
T10619: Improved
T2414: Small change, due to order of unification, fine
T2534: A very simple case in which a change of unification order
means we get tow unsolved constraints instead of one
tc211: bizarre impredicative tests; just accept this for now
Updates Cabal and haddock submodules.
Metric Increase:
T12150
T12234
T5837
haddock.base
Metric Decrease:
haddock.compiler
haddock.Cabal
haddock.base
Merge note: This appears to break the
`UnliftedNewtypesDifficultUnification` test. It has been marked as
broken in the interest of merging.
(cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)
Diffstat (limited to 'compiler')
42 files changed, 1989 insertions, 1753 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 9eb5061b64..8d7cecafdf 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -743,8 +743,7 @@ toInteger_RDR = nameRdrName toIntegerName toRational_RDR = nameRdrName toRationalName fromIntegral_RDR = nameRdrName fromIntegralName -stringTy_RDR, fromString_RDR :: RdrName -stringTy_RDR = tcQual_RDR gHC_BASE (fsLit "String") +fromString_RDR :: RdrName fromString_RDR = nameRdrName fromStringName fromList_RDR, fromListN_RDR, toList_RDR :: RdrName @@ -1680,11 +1679,13 @@ addrPrimTyConKey, arrayPrimTyConKey, arrayArrayPrimTyConKey, boolTyConKey, mutableByteArrayPrimTyConKey, orderingTyConKey, mVarPrimTyConKey, ratioTyConKey, rationalTyConKey, realWorldTyConKey, stablePtrPrimTyConKey, stablePtrTyConKey, eqTyConKey, heqTyConKey, - smallArrayPrimTyConKey, smallMutableArrayPrimTyConKey :: Unique + smallArrayPrimTyConKey, smallMutableArrayPrimTyConKey, + stringTyConKey :: Unique addrPrimTyConKey = mkPreludeTyConUnique 1 arrayPrimTyConKey = mkPreludeTyConUnique 3 boolTyConKey = mkPreludeTyConUnique 4 byteArrayPrimTyConKey = mkPreludeTyConUnique 5 +stringTyConKey = mkPreludeTyConUnique 6 charPrimTyConKey = mkPreludeTyConUnique 7 charTyConKey = mkPreludeTyConUnique 8 doublePrimTyConKey = mkPreludeTyConUnique 9 diff --git a/compiler/GHC/Builtin/Types.hs b/compiler/GHC/Builtin/Types.hs index d51f2243ca..eed9420aa6 100644 --- a/compiler/GHC/Builtin/Types.hs +++ b/compiler/GHC/Builtin/Types.hs @@ -39,7 +39,7 @@ module GHC.Builtin.Types ( -- * Char charTyCon, charDataCon, charTyCon_RDR, - charTy, stringTy, charTyConName, + charTy, stringTy, charTyConName, stringTyCon_RDR, -- * Double doubleTyCon, doubleDataCon, doubleTy, doubleTyConName, @@ -221,6 +221,7 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they , anyTyCon , boolTyCon , charTyCon + , stringTyCon , doubleTyCon , floatTyCon , intTyCon @@ -301,11 +302,12 @@ coercibleTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Coercib coercibleDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "MkCoercible") coercibleDataConKey coercibleDataCon coercibleSCSelIdName = mkWiredInIdName gHC_TYPES (fsLit "coercible_sel") coercibleSCSelIdKey coercibleSCSelId -charTyConName, charDataConName, intTyConName, intDataConName :: Name -charTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Char") charTyConKey charTyCon -charDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "C#") charDataConKey charDataCon -intTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Int") intTyConKey intTyCon -intDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "I#") intDataConKey intDataCon +charTyConName, charDataConName, intTyConName, intDataConName, stringTyConName :: Name +charTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Char") charTyConKey charTyCon +charDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "C#") charDataConKey charDataCon +stringTyConName = mkWiredInTyConName UserSyntax gHC_BASE (fsLit "String") stringTyConKey stringTyCon +intTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Int") intTyConKey intTyCon +intDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "I#") intDataConKey intDataCon boolTyConName, falseDataConName, trueDataConName :: Name boolTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Bool") boolTyConKey boolTyCon @@ -507,13 +509,14 @@ vecElemDataConNames = zipWith3Lazy mk_special_dc_name mk_special_dc_name :: FastString -> Unique -> DataCon -> Name mk_special_dc_name fs u dc = mkWiredInDataConName UserSyntax gHC_TYPES fs u dc -boolTyCon_RDR, false_RDR, true_RDR, intTyCon_RDR, charTyCon_RDR, +boolTyCon_RDR, false_RDR, true_RDR, intTyCon_RDR, charTyCon_RDR, stringTyCon_RDR, intDataCon_RDR, listTyCon_RDR, consDataCon_RDR :: RdrName boolTyCon_RDR = nameRdrName boolTyConName false_RDR = nameRdrName falseDataConName true_RDR = nameRdrName trueDataConName intTyCon_RDR = nameRdrName intTyConName charTyCon_RDR = nameRdrName charTyConName +stringTyCon_RDR = nameRdrName stringTyConName intDataCon_RDR = nameRdrName intDataConName listTyCon_RDR = nameRdrName listTyConName consDataCon_RDR = nameRdrName consDataConName @@ -1402,7 +1405,15 @@ charDataCon :: DataCon charDataCon = pcDataCon charDataConName [] [charPrimTy] charTyCon stringTy :: Type -stringTy = mkListTy charTy -- convenience only +stringTy = mkTyConApp stringTyCon [] + +stringTyCon :: TyCon +-- We have this wired-in so that Haskell literal strings +-- get type String (in hsLitType), which in turn influences +-- inferred types and error messages +stringTyCon = buildSynTyCon stringTyConName + [] liftedTypeKind [] + (mkListTy charTy) intTy :: Type intTy = mkTyConTy intTyCon diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 9aa8ea5e2c..b5e7770ed3 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -262,6 +262,7 @@ tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var]) -- forall a _1 _2. F _1 [a] _2 = ... -- -- This is a rather disgusting function +-- See Note [Wildcard names] in GHC.Tc.Gen.HsType tidyCoAxBndrsForUser init_env tcvs = (tidy_env, reverse tidy_bndrs) where diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index f06ae70a4e..4c9f99a6a7 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -112,7 +112,7 @@ module GHC.Core.Type ( isCoercionTy_maybe, isForAllTy, isForAllTy_ty, isForAllTy_co, isPiTy, isTauTy, isFamFreeTy, - isCoVarType, + isCoVarType, isAtomicTy, isValidJoinPointType, tyConAppNeedsKindSig, @@ -812,7 +812,7 @@ mkAppTy ty1 ty2 = AppTy ty1 ty2 -- Here Id is partially applied in the type sig for Foo, -- but once the type synonyms are expanded all is well -- - -- Moreover in GHC.Tc.Types.tcInferApps we build up a type + -- Moreover in GHC.Tc.Types.tcInferTyApps we build up a type -- (T t1 t2 t3) one argument at a type, thus forming -- (T t1), (T t1 t2), etc @@ -1875,6 +1875,20 @@ isTauTy (ForAllTy {}) = False isTauTy (CastTy ty _) = isTauTy ty isTauTy (CoercionTy _) = False -- Not sure about this +isAtomicTy :: Type -> Bool +-- True if the type is just a single token, and can be printed compactly +-- Used when deciding how to lay out type error messages; see the +-- call in GHC.Tc.Errors +isAtomicTy (TyVarTy {}) = True +isAtomicTy (LitTy {}) = True +isAtomicTy (TyConApp _ []) = True + +isAtomicTy ty | isLiftedTypeKind ty = True + -- 'Type' prints compactly as * + -- See GHC.Iface.Type.ppr_kind_type + +isAtomicTy _ = False + {- %************************************************************************ %* * diff --git a/compiler/GHC/Driver/Main.hs b/compiler/GHC/Driver/Main.hs index 960b7d9c51..4c86f17ac1 100644 --- a/compiler/GHC/Driver/Main.hs +++ b/compiler/GHC/Driver/Main.hs @@ -1434,7 +1434,7 @@ hscGenHardCode hsc_env cgguts location output_filename = do ------------------ Code output ----------------------- rawcmms0 <- {-# SCC "cmmToRawCmm" #-} - lookupHook cmmToRawCmmHook + lookupHook (\x -> cmmToRawCmmHook x) (\dflg _ -> cmmToRawCmm dflg) dflags dflags (Just this_mod) cmms let dump a = do @@ -1506,7 +1506,7 @@ hscCompileCmmFile hsc_env filename output_filename = runHsc hsc_env $ do unless (null cmmgroup) $ dumpIfSet_dyn dflags Opt_D_dump_cmm "Output Cmm" FormatCMM (ppr cmmgroup) - rawCmms <- lookupHook cmmToRawCmmHook + rawCmms <- lookupHook (\x -> cmmToRawCmmHook x) (\dflgs _ -> cmmToRawCmm dflgs) dflags dflags Nothing (Stream.yield cmmgroup) _ <- codeOutput dflags cmm_mod output_filename no_loc NoStubs [] [] rawCmms diff --git a/compiler/GHC/Hs/Binds.hs b/compiler/GHC/Hs/Binds.hs index 0f4a16c98e..25bcae6ce6 100644 --- a/compiler/GHC/Hs/Binds.hs +++ b/compiler/GHC/Hs/Binds.hs @@ -738,8 +738,9 @@ ppr_monobind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dictvars = sdocOption sdocPrintTypecheckerElaboration $ \case False -> pprLHsBinds val_binds True -> -- Show extra information (bug number: #10662) - hang (text "AbsBinds" <+> brackets (interpp'SP tyvars) - <+> brackets (interpp'SP dictvars)) + hang (text "AbsBinds" + <+> sep [ brackets (interpp'SP tyvars) + , brackets (interpp'SP dictvars) ]) 2 $ braces $ vcat [ text "Exports:" <+> brackets (sep (punctuate comma (map ppr exports))) @@ -751,7 +752,7 @@ ppr_monobind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dictvars instance OutputableBndrId p => Outputable (ABExport (GhcPass p)) where ppr (ABE { abe_wrap = wrap, abe_poly = gbl, abe_mono = lcl, abe_prags = prags }) - = vcat [ ppr gbl <+> text "<=" <+> ppr lcl + = vcat [ sep [ ppr gbl, nest 2 (text "<=" <+> ppr lcl) ] , nest 2 (pprTcSpecPrags prags) , pprIfTc @p $ nest 2 (text "wrap:" <+> ppr wrap) ] diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs index 43e131ce0c..8dfc317cd9 100644 --- a/compiler/GHC/Hs/Type.hs +++ b/compiler/GHC/Hs/Type.hs @@ -213,8 +213,8 @@ A wildcard in a type can be * An anonymous wildcard, written '_' In HsType this is represented by HsWildCardTy. - The renamer leaves it untouched, and it is later given fresh meta tyvars in - the typechecker. + The renamer leaves it untouched, and it is later given a fresh + meta tyvar in the typechecker. * A named wildcard, written '_a', '_foo', etc @@ -597,6 +597,7 @@ data HsTyVarBndr flag pass flag (Located (IdP pass)) -- See Note [Located RdrNames] in GHC.Hs.Expr + | KindedTyVar (XKindedTyVar pass) flag diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs index e24eb50d51..4c30aed8ff 100644 --- a/compiler/GHC/HsToCore/Binds.hs +++ b/compiler/GHC/HsToCore/Binds.hs @@ -160,6 +160,7 @@ dsHsBind dflags b@(FunBind { fun_id = L loc fun matchWrapper (mkPrefixFunRhs (L loc (idName fun))) Nothing matches + ; core_wrap <- dsHsWrapper co_fn ; let body' = mkOptTickBox tick body rhs = core_wrap (mkLams args body') @@ -197,7 +198,11 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts , abs_exports = exports , abs_ev_binds = ev_binds , abs_binds = binds, abs_sig = has_sig }) - = do { ds_binds <- addTyCsDs FromSource (listToBag dicts) (dsLHsBinds binds) + = do { ds_binds <- addTyCsDs FromSource (listToBag dicts) $ + dsLHsBinds binds + -- addTyCsDs: push type constraints deeper + -- for inner pattern match check + -- See Check, Note [Type and Term Equality Propagation] ; ds_ev_binds <- dsTcEvBinds_s ev_binds diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs index f9de7c8282..ef56c35845 100644 --- a/compiler/GHC/HsToCore/PmCheck.hs +++ b/compiler/GHC/HsToCore/PmCheck.hs @@ -27,7 +27,7 @@ import GHC.Prelude import GHC.HsToCore.PmCheck.Types import GHC.HsToCore.PmCheck.Oracle import GHC.HsToCore.PmCheck.Ppr -import GHC.Types.Basic (Origin, isGenerated) +import GHC.Types.Basic (Origin(..), isGenerated) import GHC.Core (CoreExpr, Expr(Var,App)) import GHC.Data.FastString (unpackFS, lengthFS) import GHC.Driver.Session diff --git a/compiler/GHC/Iface/Load.hs b/compiler/GHC/Iface/Load.hs index ef69e97605..f21dc1e7a1 100644 --- a/compiler/GHC/Iface/Load.hs +++ b/compiler/GHC/Iface/Load.hs @@ -529,7 +529,7 @@ loadInterface doc_str mod from ; -- invoke plugins with *full* interface, not final_iface, to ensure -- that plugins have access to declarations, etc. - res <- withPlugins dflags interfaceLoadAction iface + res <- withPlugins dflags (\p -> interfaceLoadAction p) iface ; return (Succeeded res) }}}} diff --git a/compiler/GHC/Rename/Splice.hs b/compiler/GHC/Rename/Splice.hs index 78d943bed8..eaee84119b 100644 --- a/compiler/GHC/Rename/Splice.hs +++ b/compiler/GHC/Rename/Splice.hs @@ -48,7 +48,7 @@ import GHC.Driver.Hooks import GHC.Builtin.Names.TH ( quoteExpName, quotePatName, quoteDecName, quoteTypeName , decsQTyConName, expQTyConName, patQTyConName, typeQTyConName, ) -import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckPolyExpr ) import {-# SOURCE #-} GHC.Tc.Gen.Splice ( runMetaD , runMetaE @@ -324,7 +324,7 @@ runRnSplice flavour run_meta ppr_res splice ; meta_exp_ty <- tcMetaTy meta_ty_name ; zonked_q_expr <- zonkTopLExpr =<< tcTopSpliceExpr Untyped - (tcCheckExpr the_expr meta_exp_ty) + (tcCheckPolyExpr the_expr meta_exp_ty) -- Run the expression ; mod_finalizers_ref <- newTcRef [] diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index e2a7f5f251..41bc8cd269 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -221,6 +221,7 @@ report_unsolved type_errors expr_holes , text "Wanted:" <+> ppr wanted ] ; warn_redundant <- woptM Opt_WarnRedundantConstraints + ; exp_syns <- goptM Opt_PrintExpandedSynonyms ; let err_ctxt = CEC { cec_encl = [] , cec_tidy = tidy_env , cec_defer_type_errors = type_errors @@ -234,6 +235,7 @@ report_unsolved type_errors expr_holes -- See #15539 and c.f. setting ic_status -- in GHC.Tc.Solver.setImplicationStatus , cec_warn_redundant = warn_redundant + , cec_expand_syns = exp_syns , cec_binds = binds_var } ; tc_lvl <- getTcLevel @@ -337,6 +339,7 @@ data ReportErrCtxt , cec_out_of_scope_holes :: HoleChoice -- Out of scope holes , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints + , cec_expand_syns :: Bool -- True <=> -fprint-expanded-synonyms , cec_suppress :: Bool -- True <=> More important errors have occurred, -- so create bindings if need be, but @@ -351,6 +354,7 @@ instance Outputable ReportErrCtxt where , cec_type_holes = th , cec_out_of_scope_holes = osh , cec_warn_redundant = wr + , cec_expand_syns = es , cec_suppress = sup }) = text "CEC" <+> braces (vcat [ text "cec_binds" <+> equals <+> ppr bvar @@ -359,6 +363,7 @@ instance Outputable ReportErrCtxt where , text "cec_type_holes" <+> equals <+> ppr th , text "cec_out_of_scope_holes" <+> equals <+> ppr osh , text "cec_warn_redundant" <+> equals <+> ppr wr + , text "cec_expand_syns" <+> equals <+> ppr es , text "cec_suppress" <+> equals <+> ppr sup ]) -- | Returns True <=> the ReportErrCtxt indicates that something is deferred @@ -403,7 +408,7 @@ previously suppressed. (e.g. partial-sigs/should_fail/T14584) -} reportImplic :: ReportErrCtxt -> Implication -> TcM () -reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope +reportImplic ctxt implic@(Implic { ic_skols = tvs , ic_given = given , ic_wanted = wanted, ic_binds = evb , ic_status = status, ic_info = info @@ -417,10 +422,12 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope | otherwise = do { traceTc "reportImplic" (ppr implic') + ; when bad_telescope $ reportBadTelescope ctxt tcl_env info tvs + -- Do /not/ use the tidied tvs because then are in the + -- wrong order, so tidying will rename things wrongly ; reportWanteds ctxt' tc_lvl wanted ; when (cec_warn_redundant ctxt) $ - warnRedundantConstraints ctxt' tcl_env info' dead_givens - ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs } + warnRedundantConstraints ctxt' tcl_env info' dead_givens } where tcl_env = ic_env implic insoluble = isInsolubleStatus status @@ -492,8 +499,8 @@ warnRedundantConstraints ctxt env info ev_vars improving pred -- (transSuperClasses p) does not include p = any isImprovementPred (pred : transSuperClasses pred) -reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM () -reportBadTelescope ctxt env (Just telescope) skols +reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM () +reportBadTelescope ctxt env (ForAllSkol _ telescope) skols = do { msg <- mkErrorReport ctxt env (important doc) ; reportError msg } where @@ -503,8 +510,8 @@ reportBadTelescope ctxt env (Just telescope) skols sorted_tvs = scopedSort skols -reportBadTelescope _ _ Nothing skols - = pprPanic "reportBadTelescope" (ppr skols) +reportBadTelescope _ _ skol_info skols + = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols) {- Note [Redundant constraints in instance decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -752,8 +759,7 @@ mkGivenErrorReporter ctxt cts report = important inaccessible_msg `mappend` mk_relevant_bindings binds_msg - ; err <- mkEqErr_help dflags ctxt report ct' - Nothing ty1 ty2 + ; err <- mkEqErr_help dflags ctxt report ct' ty1 ty2 ; traceTc "mkGivenErrorReporter" (ppr ct) ; reportWarning (Reason Opt_WarnInaccessibleCode) err } @@ -1126,7 +1132,7 @@ mkIrredErr ctxt cts ; let orig = ctOrigin ct1 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig) ; mkErrorMsgFromCt ctxt ct1 $ - important msg `mappend` mk_relevant_bindings binds_msg } + msg `mappend` mk_relevant_bindings binds_msg } where (ct1:_) = cts @@ -1276,14 +1282,14 @@ mkIPErr ctxt cts preds = map ctPred cts givens = getUserGivens ctxt msg | null givens - = addArising orig $ + = important $ addArising orig $ sep [ text "Unbound implicit parameter" <> plural cts , nest 2 (pprParendTheta preds) ] | otherwise = couldNotDeduce givens (preds, orig) ; mkErrorMsgFromCt ctxt ct1 $ - important msg `mappend` mk_relevant_bindings binds_msg } + msg `mappend` mk_relevant_bindings binds_msg } where (ct1:_) = cts @@ -1356,56 +1362,17 @@ mkEqErr1 ctxt ct -- Wanted or derived; = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct ; rdr_env <- getGlobalRdrEnv ; fam_envs <- tcGetFamInstEnvs - ; exp_syns <- goptM Opt_PrintExpandedSynonyms - ; let (keep_going, is_oriented, wanted_msg) - = mk_wanted_extra (ctLoc ct) exp_syns - coercible_msg = case ctEqRel ct of + ; let coercible_msg = case ctEqRel ct of NomEq -> empty ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2 ; dflags <- getDynFlags - ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going) - ; let report = mconcat [important wanted_msg, important coercible_msg, - mk_relevant_bindings binds_msg] - ; if keep_going - then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2 - else mkErrorMsgFromCt ctxt ct report } + ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct)) + ; let report = mconcat [ important coercible_msg + , mk_relevant_bindings binds_msg] + ; mkEqErr_help dflags ctxt report ct ty1 ty2 } where (ty1, ty2) = getEqPredTys (ctPred ct) - -- If the types in the error message are the same as the types - -- we are unifying, don't add the extra expected/actual message - mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc) - mk_wanted_extra loc expandSyns - = case ctLocOrigin loc of - orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig - t_or_k expandSyns - where - t_or_k = ctLocTypeOrKind_maybe loc - - KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k - -> (True, Nothing, msg1 $$ msg2) - where - sub_what = case sub_t_or_k of Just KindLevel -> text "kinds" - _ -> text "types" - msg1 = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions -> - case mb_cty2 of - Just cty2 - | printExplicitCoercions - || not (cty1 `pickyEqType` cty2) - -> hang (text "When matching" <+> sub_what) - 2 (vcat [ ppr cty1 <+> dcolon <+> - ppr (tcTypeKind cty1) - , ppr cty2 <+> dcolon <+> - ppr (tcTypeKind cty2) ]) - _ -> text "When matching the kind of" <+> quotes (ppr cty1) - msg2 = case sub_o of - TypeEqOrigin {} - | Just cty2 <- mb_cty2 -> - thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k - expandSyns) - _ -> empty - _ -> (True, Nothing, empty) - -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint -- is left over. mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs @@ -1453,76 +1420,43 @@ mkCoercibleExplanation rdr_env fam_envs ty1 ty2 | otherwise = False -{- --- | Make a listing of role signatures for all the parameterised tycons --- used in the provided types - - --- SLPJ Jun 15: I could not convince myself that these hints were really --- useful. Maybe they are, but I think we need more work to make them --- actually helpful. -mkRoleSigs :: Type -> Type -> SDoc -mkRoleSigs ty1 ty2 - = ppUnless (null role_sigs) $ - hang (text "Relevant role signatures:") - 2 (vcat role_sigs) - where - tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2 - role_sigs = mapMaybe ppr_role_sig tcs - - ppr_role_sig tc - | null roles -- if there are no parameters, don't bother printing - = Nothing - | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc. - = Nothing - | otherwise - = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles - where - roles = tyConRoles tc --} - mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -- Nothing <=> not sure -> TcType -> TcType -> TcM ErrMsg -mkEqErr_help dflags ctxt report ct oriented ty1 ty2 +mkEqErr_help dflags ctxt report ct ty1 ty2 | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1 - = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 + = mkTyVarEqErr dflags ctxt report ct tv1 ty2 | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2 - = mkTyVarEqErr dflags ctxt report ct swapped tv2 ty1 + = mkTyVarEqErr dflags ctxt report ct tv2 ty1 | otherwise - = reportEqErr ctxt report ct oriented ty1 ty2 - where - swapped = fmap flipSwap oriented + = reportEqErr ctxt report ct ty1 ty2 reportEqErr :: ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -- Nothing <=> not sure -> TcType -> TcType -> TcM ErrMsg -reportEqErr ctxt report ct oriented ty1 ty2 +reportEqErr ctxt report ct ty1 ty2 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo]) - where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2 - eqInfo = important $ mkEqInfoMsg ct ty1 ty2 + where + misMatch = misMatchOrCND False ctxt ct ty1 ty2 + eqInfo = mkEqInfoMsg ct ty1 ty2 mkTyVarEqErr, mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg + -> TcTyVar -> TcType -> TcM ErrMsg -- tv1 and ty2 are already tidied -mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 +mkTyVarEqErr dflags ctxt report ct tv1 ty2 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2) - ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 } + ; mkTyVarEqErr' dflags ctxt report ct tv1 ty2 } -mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 - | not insoluble_occurs_check -- See Note [Occurs check wins] - , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would - -- be oriented the other way round; - -- see GHC.Tc.Solver.Canonical.canEqTyVarTyVar +mkTyVarEqErr' dflags ctxt report ct tv1 ty2 + | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar; we would have + -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) || ctEqRel ct == ReprEq - -- the cases below don't really apply to ReprEq (except occurs check) + -- The cases below don't really apply to ReprEq (except occurs check) = mkErrorMsgFromCt ctxt ct $ mconcat - [ important $ misMatchOrCND ctxt ct oriented ty1 ty2 - , important $ extraTyVarEqInfo ctxt tv1 ty2 + [ headline_msg + , extraTyVarEqInfo ctxt tv1 ty2 , report ] @@ -1531,11 +1465,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it -- See Note [Occurs check error] in GHC.Tc.Solver.Canonical - = do { let main_msg = addArising (ctOrigin ct) $ - hang (text "Occurs check: cannot construct the infinite" <+> what <> colon) - 2 (sep [ppr ty1, char '~', ppr ty2]) - - extra2 = important $ mkEqInfoMsg ct ty1 ty2 + = do { let extra2 = mkEqInfoMsg ct ty1 ty2 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $ filter isTyVar $ @@ -1549,17 +1479,16 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) ; mkErrorMsgFromCt ctxt ct $ - mconcat [important main_msg, extra2, extra3, report] } + mconcat [headline_msg, extra2, extra3, report] } | MTVU_Bad <- occ_check_expand = do { let msg = vcat [ text "Cannot instantiate unification variable" <+> quotes (ppr tv1) - , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) - , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ] + , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ] -- Unlike the other reports, this discards the old 'report_important' -- instead of augmenting it. This is because the details are not likely -- to be helpful since this is just an unimplemented feature. - ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } } + ; mkErrorMsgFromCt ctxt ct $ mconcat [ headline_msg, important msg, report ] } -- If the immediately-enclosing implication has 'tv' a skolem, and -- we know by now its an InferSkol kind of skolem, then presumably @@ -1569,8 +1498,8 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_skols = skols } <- implic , tv1 `elem` skols = mkErrorMsgFromCt ctxt ct $ mconcat - [ important $ misMatchMsg ct oriented ty1 ty2 - , important $ extraTyVarEqInfo ctxt tv1 ty2 + [ misMatchMsg ctxt ct ty1 ty2 + , extraTyVarEqInfo ctxt tv1 ty2 , report ] @@ -1579,7 +1508,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_skols = skols, ic_info = skol_info } <- implic , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols , not (null esc_skols) - = do { let msg = important $ misMatchMsg ct oriented ty1 ty2 + = do { let msg = misMatchMsg ctxt ct ty1 ty2 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols <+> pprQuotedList esc_skols , text "would escape" <+> @@ -1607,7 +1536,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic = ASSERT2( not (isTouchableMetaTyVar lvl tv1) , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables] - do { let msg = important $ misMatchMsg ct oriented ty1 ty2 + do { let msg = misMatchMsg ctxt ct ty1 ty2 tclvl_extra = important $ nest 2 $ sep [ quotes (ppr tv1) <+> text "is untouchable" @@ -1615,33 +1544,38 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , nest 2 $ text "bound by" <+> ppr skol_info , nest 2 $ text "at" <+> ppr (tcl_loc (ic_env implic)) ] - tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2 - add_sig = important $ suggestAddSig ctxt ty1 ty2 + tv_extra = extraTyVarEqInfo ctxt tv1 ty2 + add_sig = suggestAddSig ctxt ty1 ty2 ; mkErrorMsgFromCt ctxt ct $ mconcat [msg, tclvl_extra, tv_extra, add_sig, report] } | otherwise - = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2 + = reportEqErr ctxt report ct (mkTyVarTy tv1) ty2 -- This *can* happen (#6123, and test T2627b) -- Consider an ambiguous top-level constraint (a ~ F a) -- Not an occurs check, because F is a type function. where + headline_msg = misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2 + ty1 = mkTyVarTy tv1 occ_check_expand = occCheckForErrors dflags tv1 ty2 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2 - what = case ctLocTypeOrKind_maybe (ctLoc ct) of - Just KindLevel -> text "kind" - _ -> text "type" + what = text $ levelString $ + ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel -mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc +levelString :: TypeOrKind -> String +levelString TypeLevel = "type" +levelString KindLevel = "kind" + +mkEqInfoMsg :: Ct -> TcType -> TcType -> Report -- Report (a) ambiguity if either side is a type function application -- e.g. F a0 ~ Int -- (b) warning about injectivity if both sides are the same -- type function application F a ~ F b -- See Note [Non-injective type functions] mkEqInfoMsg ct ty1 ty2 - = tyfun_msg $$ ambig_msg + = important (tyfun_msg $$ ambig_msg) where mb_fun1 = isTyFun_maybe ty1 mb_fun2 = isTyFun_maybe ty2 @@ -1669,29 +1603,34 @@ isUserSkolem ctxt tv is_user_skol_info (InferSkol {}) = False is_user_skol_info _ = True -misMatchOrCND :: ReportErrCtxt -> Ct - -> Maybe SwapFlag -> TcType -> TcType -> SDoc +misMatchOrCND :: Bool -> ReportErrCtxt -> Ct + -> TcType -> TcType -> Report -- If oriented then ty1 is actual, ty2 is expected -misMatchOrCND ctxt ct oriented ty1 ty2 - | null givens || - (isRigidTy ty1 && isRigidTy ty2) || - isGivenCt ct - -- If the equality is unconditionally insoluble - -- or there is no context, don't report the context - = misMatchMsg ct oriented ty1 ty2 +misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2 + | insoluble_occurs_check -- See Note [Insoluble occurs check] + || (isRigidTy ty1 && isRigidTy ty2) + || isGivenCt ct + || null givens + = -- If the equality is unconditionally insoluble + -- or there is no context, don't report the context + misMatchMsg ctxt ct ty1 ty2 + | otherwise - = couldNotDeduce givens ([eq_pred], orig) + = mconcat [ couldNotDeduce givens ([eq_pred], orig) + , important $ mk_supplementary_ea_msg ctxt level ty1 ty2 orig ] where ev = ctEvidence ct eq_pred = ctEvPred ev orig = ctEvOrigin ev + level = ctLocTypeOrKind_maybe (ctEvLoc ev) `orElse` TypeLevel givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)] -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] -couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc +couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> Report couldNotDeduce givens (wanteds, orig) - = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds) + = important $ + vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds) , vcat (pp_givens givens)] pp_givens :: [UserGiven] -> [SDoc] @@ -1763,11 +1702,11 @@ addition to superclasses (see Note [Remove redundant provided dicts] in GHC.Tc.TyCl.PatSyn). -} -extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc +extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> Report -- Add on extra info about skolem constants -- NB: The types themselves are already tidied extraTyVarEqInfo ctxt tv1 ty2 - = extraTyVarInfo ctxt tv1 $$ ty_extra ty2 + = important (extraTyVarInfo ctxt tv1 $$ ty_extra ty2) where ty_extra ty = case tcGetCastedTyVar_maybe ty of Just (tv, _) -> extraTyVarInfo ctxt tv @@ -1781,15 +1720,15 @@ extraTyVarInfo ctxt tv RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem" MetaTv {} -> empty -suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc +suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report -- See Note [Suggest adding a type signature] suggestAddSig ctxt ty1 ty2 | null inferred_bndrs - = empty + = mempty | [bndr] <- inferred_bndrs - = text "Possible fix: add a type signature for" <+> quotes (ppr bndr) + = important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr) | otherwise - = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs) + = important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs) where inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2) get_inf ty | Just tv <- tcGetTyVar_maybe ty @@ -1800,47 +1739,55 @@ suggestAddSig ctxt ty1 ty2 = [] -------------------- -misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc +misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report -- Types are already tidy -- If oriented then ty1 is actual, ty2 is expected -misMatchMsg ct oriented ty1 ty2 - | Just NotSwapped <- oriented - = misMatchMsg ct (Just IsSwapped) ty2 ty1 - - -- These next two cases are when we're about to report, e.g., that - -- 'LiftedRep doesn't match 'VoidRep. Much better just to say - -- lifted vs. unlifted - | isLiftedRuntimeRep ty1 - = lifted_vs_unlifted - - | isLiftedRuntimeRep ty2 - = lifted_vs_unlifted - - | otherwise -- So now we have Nothing or (Just IsSwapped) - -- For some reason we treat Nothing like IsSwapped - = addArising orig $ - pprWithExplicitKindsWhenMismatch ty1 ty2 (ctOrigin ct) $ +misMatchMsg ctxt ct ty1 ty2 + = important $ + addArising orig $ + pprWithExplicitKindsWhenMismatch ty1 ty2 orig $ + sep [ case orig of + TypeEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig + KindEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig + _ -> headline_eq_msg False ct ty1 ty2 + , sameOccExtra ty2 ty1 ] + where + orig = ctOrigin ct + +headline_eq_msg :: Bool -> Ct -> Type -> Type -> SDoc +-- Generates the main "Could't match 't1' against 't2' +-- headline message +headline_eq_msg add_ea ct ty1 ty2 + + | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) || + (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) + = text "Couldn't match a lifted type with an unlifted type" + + | isAtomicTy ty1 || isAtomicTy ty2 + = -- Print with quotes sep [ text herald1 <+> quotes (ppr ty1) , nest padding $ - text herald2 <+> quotes (ppr ty2) - , sameOccExtra ty2 ty1 ] + text herald2 <+> quotes (ppr ty2) ] + + | otherwise + = -- Print with vertical layout + vcat [ text herald1 <> colon <+> ppr ty1 + , nest padding $ + text herald2 <> colon <+> ppr ty2 ] where herald1 = conc [ "Couldn't match" - , if is_repr then "representation of" else "" - , if is_oriented then "expected" else "" + , if is_repr then "representation of" else "" + , if add_ea then "expected" else "" , what ] herald2 = conc [ "with" - , if is_repr then "that of" else "" - , if is_oriented then ("actual " ++ what) else "" ] + , if is_repr then "that of" else "" + , if add_ea then ("actual " ++ what) else "" ] + padding = length herald1 - length herald2 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False } - is_oriented = isJust oriented - orig = ctOrigin ct - what = case ctLocTypeOrKind_maybe (ctLoc ct) of - Just KindLevel -> "kind" - _ -> "type" + what = levelString (ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel) conc :: [String] -> String conc = foldr1 add_space @@ -1850,114 +1797,49 @@ misMatchMsg ct oriented ty1 ty2 | null s2 = s1 | otherwise = s1 ++ (' ' : s2) - lifted_vs_unlifted - = addArising orig $ - text "Couldn't match a lifted type with an unlifted type" --- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a --- type mismatch occurs to due invisible kind arguments. --- --- This function first checks to see if the 'CtOrigin' argument is a --- 'TypeEqOrigin', and if so, uses the expected/actual types from that to --- check for a kind mismatch (as these types typically have more surrounding --- types and are likelier to be able to glean information about whether a --- mismatch occurred in an invisible argument position or not). If the --- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types --- themselves. -pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin - -> SDoc -> SDoc -pprWithExplicitKindsWhenMismatch ty1 ty2 ct - = pprWithExplicitKindsWhen show_kinds - where - (act_ty, exp_ty) = case ct of - TypeEqOrigin { uo_actual = act - , uo_expected = exp } -> (act, exp) - _ -> (ty1, ty2) - show_kinds = tcEqTypeVis act_ty exp_ty - -- True when the visible bit of the types look the same, - -- so we want to show the kinds in the displayed type - -mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool - -> (Bool, Maybe SwapFlag, SDoc) --- NotSwapped means (actual, expected), IsSwapped is the reverse --- First return val is whether or not to print a herald above this msg -mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act +tk_eq_msg :: ReportErrCtxt + -> Ct -> Type -> Type -> CtOrigin -> SDoc +tk_eq_msg ctxt ct ty1 ty2 orig@(TypeEqOrigin { uo_actual = act , uo_expected = exp - , uo_thing = maybe_thing }) - m_level printExpanded - | KindLevel <- level, occurs_check_error = (True, Nothing, empty) - | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2) - | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3) - | tcIsLiftedTypeKind exp = (False, Nothing, msg4) - | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1) - | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th) - | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty) - | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty) - | otherwise = (True, Nothing, msg1) - where - level = m_level `orElse` TypeLevel + , uo_thing = mb_thing }) + -- We can use the TypeEqOrigin to + -- improve the error message quite a lot + + | isUnliftedTypeKind act, isLiftedTypeKind exp + = sep [ text "Expecting a lifted type, but" + , thing_msg mb_thing (text "an") (text "unlifted") ] + + | isLiftedTypeKind act, isUnliftedTypeKind exp + = sep [ text "Expecting an unlifted type, but" + , thing_msg mb_thing (text "a") (text "lifted") ] + + | tcIsLiftedTypeKind exp + = maybe_num_args_msg $$ + sep [ text "Expected a type, but" + , case mb_thing of + Nothing -> text "found something with kind" + Just thing -> quotes thing <+> text "has kind" + , quotes (pprWithTYPE act) ] + + | Just nargs_msg <- num_args_msg + = nargs_msg $$ + mk_ea_msg ctxt (Just ct) level orig + + | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $ + ea_looks_same ty1 ty2 exp act + = mk_ea_msg ctxt (Just ct) level orig + + | otherwise -- The mismatched types are /inside/ exp and act + = vcat [ headline_eq_msg False ct ty1 ty2 + , mk_ea_msg ctxt Nothing level orig ] - occurs_check_error - | Just tv <- tcGetTyVar_maybe ty1 - , tv `elemVarSet` tyCoVarsOfType ty2 - = True - | Just tv <- tcGetTyVar_maybe ty2 - , tv `elemVarSet` tyCoVarsOfType ty1 - = True - | otherwise - = False - - sort = case level of - TypeLevel -> text "type" - KindLevel -> text "kind" - - msg1 = case level of - KindLevel - | Just th <- maybe_thing - -> msg5 th - - _ | not (act `pickyEqType` exp) - -> pprWithExplicitKindsWhenMismatch ty1 ty2 ct $ - vcat [ text "Expected" <+> sort <> colon <+> ppr exp - , text " Actual" <+> sort <> colon <+> ppr act - , if printExpanded then expandedTys else empty ] - - | otherwise - -> empty - - thing_msg = case maybe_thing of - Just thing -> \_ levity -> - quotes thing <+> text "is" <+> levity - Nothing -> \vowel levity -> - text "got a" <> - (if vowel then char 'n' else empty) <+> - levity <+> - text "type" - msg2 = sep [ text "Expecting a lifted type, but" - , thing_msg True (text "unlifted") ] - msg3 = sep [ text "Expecting an unlifted type, but" - , thing_msg False (text "lifted") ] - msg4 = maybe_num_args_msg $$ - sep [ text "Expected a type, but" - , maybe (text "found something with kind") - (\thing -> quotes thing <+> text "has kind") - maybe_thing - , quotes (pprWithTYPE act) ] - - msg5 th = pprWithExplicitKindsWhenMismatch ty1 ty2 ct $ - hang (text "Expected" <+> kind_desc <> comma) - 2 (text "but" <+> quotes th <+> text "has kind" <+> - quotes (ppr act)) - where - kind_desc | tcIsConstraintKind exp = text "a constraint" - - -- TYPE t0 - | Just arg <- kindRep_maybe exp - , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case - True -> text "kind" <+> quotes (ppr exp) - False -> text "a type" + where + ct_loc = ctLoc ct + level = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel - | otherwise = text "kind" <+> quotes (ppr exp) + thing_msg (Just thing) _ levity = quotes thing <+> text "is" <+> levity + thing_msg Nothing an levity = text "got" <+> an <+> levity <+> text "type" num_args_msg = case level of KindLevel @@ -1970,7 +1852,7 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act case n_act - n_exp of n | n > 0 -- we don't know how many args there are, so don't -- recommend removing args that aren't - , Just thing <- maybe_thing + , Just thing <- mb_thing -> Just $ text "Expecting" <+> speakN (abs n) <+> more <+> quotes thing where @@ -1981,25 +1863,125 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act _ -> Nothing - maybe_num_args_msg = case num_args_msg of - Nothing -> empty - Just m -> m + maybe_num_args_msg = num_args_msg `orElse` empty count_args ty = count isVisibleBinder $ fst $ splitPiTys ty - expandedTys = - ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat - [ text "Type synonyms expanded:" - , text "Expected type:" <+> ppr expTy1 - , text " Actual type:" <+> ppr expTy2 - ] +tk_eq_msg ctxt ct ty1 ty2 + (KindEqOrigin cty1 mb_cty2 sub_o mb_sub_t_or_k) + = vcat [ headline_eq_msg False ct ty1 ty2 + , supplementary_msg ] + where + sub_t_or_k = mb_sub_t_or_k `orElse` TypeLevel + sub_whats = text (levelString sub_t_or_k) <> char 's' + -- "types" or "kinds" + + supplementary_msg + = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions -> + case mb_cty2 of + Just cty2 + | printExplicitCoercions + || not (cty1 `pickyEqType` cty2) + -> vcat [ hang (text "When matching" <+> sub_whats) + 2 (vcat [ ppr cty1 <+> dcolon <+> + ppr (tcTypeKind cty1) + , ppr cty2 <+> dcolon <+> + ppr (tcTypeKind cty2) ]) + , mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o ] + _ -> text "When matching the kind of" <+> quotes (ppr cty1) + +tk_eq_msg _ _ _ _ _ = panic "typeeq_mismatch_msg" + +ea_looks_same :: Type -> Type -> Type -> Type -> Bool +-- True if the faulting types (ty1, ty2) look the same as +-- the expected/actual types (exp, act). +-- If so, we don't want to redundantly report the latter +ea_looks_same ty1 ty2 exp act + = (act `looks_same` ty1 && exp `looks_same` ty2) || + (exp `looks_same` ty1 && act `looks_same` ty2) + where + looks_same t1 t2 = t1 `pickyEqType` t2 + || t1 `eqType` liftedTypeKind && t2 `eqType` liftedTypeKind + -- pickyEqType is sensitive to synonyms, so only replies True + -- when the types really look the same. However, + -- (TYPE 'LiftedRep) and Type both print the same way. + +mk_supplementary_ea_msg :: ReportErrCtxt -> TypeOrKind + -> Type -> Type -> CtOrigin -> SDoc +mk_supplementary_ea_msg ctxt level ty1 ty2 orig + | TypeEqOrigin { uo_expected = exp, uo_actual = act } <- orig + , not (ea_looks_same ty1 ty2 exp act) + = mk_ea_msg ctxt Nothing level orig + | otherwise + = empty + +mk_ea_msg :: ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc +-- Constructs a "Couldn't match" message +-- The (Maybe Ct) says whether this is the main top-level message (Just) +-- or a supplementary message (Nothing) +mk_ea_msg ctxt at_top level + (TypeEqOrigin { uo_actual = act, uo_expected = exp, uo_thing = mb_thing }) + | Just thing <- mb_thing + , KindLevel <- level + = hang (text "Expected" <+> kind_desc <> comma) + 2 (text "but" <+> quotes thing <+> text "has kind" <+> + quotes (ppr act)) + + | otherwise + = vcat [ case at_top of + Just ct -> headline_eq_msg True ct exp act + Nothing -> supplementary_ea_msg + , ppWhen expand_syns expandedTys ] + + where + supplementary_ea_msg = vcat [ text "Expected:" <+> ppr exp + , text " Actual:" <+> ppr act ] + + kind_desc | tcIsConstraintKind exp = text "a constraint" + | Just arg <- kindRep_maybe exp -- TYPE t0 + , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case + True -> text "kind" <+> quotes (ppr exp) + False -> text "a type" + | otherwise = text "kind" <+> quotes (ppr exp) + + expand_syns = cec_expand_syns ctxt + + expandedTys = ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat + [ text "Type synonyms expanded:" + , text "Expected type:" <+> ppr expTy1 + , text " Actual type:" <+> ppr expTy2 ] (expTy1, expTy2) = expandSynonymsToMatch exp act -mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg" +mk_ea_msg _ _ _ _ = empty + +-- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a +-- type mismatch occurs to due invisible kind arguments. +-- +-- This function first checks to see if the 'CtOrigin' argument is a +-- 'TypeEqOrigin', and if so, uses the expected/actual types from that to +-- check for a kind mismatch (as these types typically have more surrounding +-- types and are likelier to be able to glean information about whether a +-- mismatch occurred in an invisible argument position or not). If the +-- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types +-- themselves. +pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin + -> SDoc -> SDoc +pprWithExplicitKindsWhenMismatch ty1 ty2 ct + = pprWithExplicitKindsWhen show_kinds + where + (act_ty, exp_ty) = case ct of + TypeEqOrigin { uo_actual = act + , uo_expected = exp } -> (act, exp) + _ -> (ty1, ty2) + show_kinds = tcEqTypeVis act_ty exp_ty + -- True when the visible bit of the types look the same, + -- so we want to show the kinds in the displayed type + + -{- Note [Insoluble occurs check wins] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Insoluble occurs check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble so we don't use it for rewriting. The Wanted is also insoluble, and we don't solve it from the Given. It's very confusing to say @@ -2009,7 +1991,8 @@ And indeed even thinking about the Givens is silly; [W] a ~ [a] is just as insoluble as Int ~ Bool. Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck) -then report it first. +then report it directly, not in the "cannot deduce X from Y" form. +This is done in misMatchOrCND (via the insoluble_occurs_check arg) (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't want to be as draconian with them.) diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs index 0639e79073..7c0eaa7912 100644 --- a/compiler/GHC/Tc/Errors/Hole.hs +++ b/compiler/GHC/Tc/Errors/Hole.hs @@ -43,7 +43,7 @@ import Data.Graph ( graphFromEdges, topSort ) import GHC.Tc.Solver ( simpl_top, runTcSDeriveds ) -import GHC.Tc.Utils.Unify ( tcSubType_NC ) +import GHC.Tc.Utils.Unify ( tcSubTypeSigma ) import GHC.HsToCore.Docs ( extractDocs ) import qualified Data.Map as Map @@ -933,7 +933,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $ -- imp is the innermost implication (imp:_) -> return (ic_tclvl imp) ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $ - tcSubType_NC ExprSigCtxt ty hole_ty + tcSubTypeSigma ExprSigCtxt ty hole_ty ; traceTc "Checking hole fit {" empty ; traceTc "wanteds are: " $ ppr wanted ; if isEmptyWC wanted && isEmptyBag th_relevant_cts diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index ef60b3cea7..c21a885970 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -14,7 +14,8 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcLExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcCheckExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp + , tcCheckId, tcCheckPolyExpr ) import GHC.Hs import GHC.Tc.Gen.Match @@ -161,7 +162,7 @@ tc_cmd env in_cmd@(HsCmdLamCase x matches) (stk, res_ty) return (mkHsCmdWrap (mkWpCastN co) (HsCmdLamCase x matches')) tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if' - = do { pred' <- tcLExpr pred (mkCheckExpType boolTy) + = do { pred' <- tcCheckMonoExpr pred boolTy ; b1' <- tcCmd env b1 res_ty ; b2' <- tcCmd env b2 res_ty ; return (HsCmdIf x NoSyntaxExprTc pred' b1' b2') @@ -179,7 +180,7 @@ tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syn ; (pred', fun') <- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty]) (mkCheckExpType r_ty) $ \ _ -> - tcLExpr pred (mkCheckExpType pred_ty) + tcCheckMonoExpr pred pred_ty ; b1' <- tcCmd env b1 res_ty ; b2' <- tcCmd env b2 res_ty @@ -206,9 +207,9 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) = addErrCtxt (cmdCtxt cmd) $ do { arg_ty <- newOpenFlexiTyVarTy ; let fun_ty = mkCmdArrTy env arg_ty res_ty - ; fun' <- select_arrow_scope (tcLExpr fun (mkCheckExpType fun_ty)) + ; fun' <- select_arrow_scope (tcCheckMonoExpr fun fun_ty) - ; arg' <- tcLExpr arg (mkCheckExpType arg_ty) + ; arg' <- tcCheckMonoExpr arg arg_ty ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) } where @@ -233,7 +234,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) = addErrCtxt (cmdCtxt cmd) $ do { arg_ty <- newOpenFlexiTyVarTy ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty) - ; arg' <- tcLExpr arg (mkCheckExpType arg_ty) + ; arg' <- tcCheckMonoExpr arg arg_ty ; return (HsCmdApp x fun' arg') } ------------------------------------------- @@ -310,7 +311,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) ; let e_ty = mkInfForAllTy alphaTyVar $ mkVisFunTys cmd_tys $ mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty - ; expr' <- tcCheckExpr expr e_ty + ; expr' <- tcCheckPolyExpr expr e_ty ; return (HsCmdArrForm x expr' f fixity cmd_args') } where diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 1870531f60..bd9d14e2d4 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -23,8 +23,9 @@ where import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun ) -import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcLExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckMonoExpr ) import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind ) + import GHC.Core (Tickish (..)) import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC)) import GHC.Driver.Session @@ -354,7 +355,7 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside = do { ty <- newOpenFlexiTyVarTy ; let p = mkStrLitTy $ hsIPNameFS ip ; ip_id <- newDict ipClass [ p, ty ] - ; expr' <- tcLExpr expr (mkCheckExpType ty) + ; expr' <- tcCheckMonoExpr expr ty ; let d = toDict ipClass p ty `fmap` expr' ; return (ip_id, (IPBind noExtField (Right ip_id) d)) } tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind" @@ -389,22 +390,25 @@ tcValBinds top_lvl binds sigs thing_inside -- It's easier to do so now, once for all the SCCs together -- because a single signature f,g :: <type> -- might relate to more than one SCC - ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $ + (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $ tcTySigs sigs - -- Extend the envt right away with all the Ids - -- declared with complete type signatures - -- Do not extend the TcBinderStack; instead - -- we extend it on a per-rhs basis in tcExtendForRhs - ; tcExtendSigIds top_lvl poly_ids $ do - { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do - { thing <- thing_inside - -- See Note [Pattern synonym builders don't yield dependencies] - -- in GHC.Rename.Bind - ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns - ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ] - ; return (extra_binds, thing) } - ; return (binds' ++ extra_binds', thing) }} + -- Extend the envt right away with all the Ids + -- declared with complete type signatures + -- Do not extend the TcBinderStack; instead + -- we extend it on a per-rhs basis in tcExtendForRhs + -- See Note [Relevant bindings and the binder stack] + ; tcExtendSigIds top_lvl poly_ids $ + do { (binds', (extra_binds', thing)) + <- tcBindGroups top_lvl sig_fn prag_fn binds $ + do { thing <- thing_inside + -- See Note [Pattern synonym builders don't yield dependencies] + -- in GHC.Rename.Bind + ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns + ; let extra_binds = [ (NonRecursive, builder) + | builder <- patsyn_builders ] + ; return (extra_binds, thing) } + ; return (binds' ++ extra_binds', thing) }} where patsyns = getPatSynBinds binds prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds) @@ -686,50 +690,60 @@ tcPolyCheck prag_fn (CompleteSig { sig_bndr = poly_id , sig_ctxt = ctxt , sig_loc = sig_loc }) - (L loc (FunBind { fun_id = (L nm_loc name) - , fun_matches = matches })) - = setSrcSpan sig_loc $ - do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc) - ; (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id - -- See Note [Instantiate sig with fresh variables] + (L bind_loc (FunBind { fun_id = L nm_loc name + , fun_matches = matches })) + = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc) ; mono_name <- newNameAt (nameOccName name) nm_loc - ; ev_vars <- newEvVars theta - ; let mono_id = mkLocalId mono_name tau - skol_info = SigSkol ctxt (idType poly_id) tv_prs - skol_tvs = map snd tv_prs - - ; (ev_binds, (co_fn, matches')) - <- checkConstraints skol_info skol_tvs ev_vars $ - tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $ - tcExtendNameTyVarEnv tv_prs $ - setSrcSpan loc $ - tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau) + ; (wrap_gen, (wrap_res, matches')) + <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems + tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty -> + -- Unwraps multiple layers; e.g + -- f :: forall a. Eq a => forall b. Ord b => blah + -- NB: tcSkolemise makes fresh type variables + -- See Note [Instantiate sig with fresh variables] + + let mono_id = mkLocalId mono_name rho_ty in + tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $ + -- Why mono_id in the BinderStack? + -- See Note [Relevant bindings and the binder stack] + + setSrcSpan bind_loc $ + tcMatchesFun (L nm_loc mono_name) matches + (mkCheckExpType rho_ty) + + -- We make a funny AbsBinds, abstracting over nothing, + -- just so we haev somewhere to put the SpecPrags. + -- Otherwise we could just use the FunBind + -- Hence poly_id2 is just a clone of poly_id; + -- We re-use mono-name, but we could equally well use a fresh one ; let prag_sigs = lookupPragEnv prag_fn name - ; spec_prags <- tcSpecPrags poly_id prag_sigs + poly_id2 = mkLocalId mono_name (idType poly_id) + ; spec_prags <- tcSpecPrags poly_id prag_sigs ; poly_id <- addInlinePrags poly_id prag_sigs ; mod <- getModule - ; tick <- funBindTicks nm_loc mono_id mod prag_sigs - ; let bind' = FunBind { fun_id = L nm_loc mono_id + ; tick <- funBindTicks nm_loc poly_id mod prag_sigs + + ; let bind' = FunBind { fun_id = L nm_loc poly_id2 , fun_matches = matches' - , fun_ext = co_fn + , fun_ext = wrap_gen <.> wrap_res , fun_tick = tick } export = ABE { abe_ext = noExtField , abe_wrap = idHsWrapper , abe_poly = poly_id - , abe_mono = mono_id + , abe_mono = poly_id2 , abe_prags = SpecPrags spec_prags } - abs_bind = L loc $ + abs_bind = L bind_loc $ AbsBinds { abs_ext = noExtField - , abs_tvs = skol_tvs - , abs_ev_vars = ev_vars - , abs_ev_binds = [ev_binds] + , abs_tvs = [] + , abs_ev_vars = [] + , abs_ev_binds = [] , abs_exports = [export] - , abs_binds = unitBag (L loc bind') + , abs_binds = unitBag (L bind_loc bind') , abs_sig = True } ; return (unitBag abs_bind, [poly_id]) } @@ -862,7 +876,7 @@ mkExport prag_fn insoluble qtvs theta -- an ambiguous type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $ - tcSubType_NC sig_ctxt sel_poly_ty poly_ty + tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures ; when warn_missing_sigs $ @@ -943,8 +957,12 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs , sig_inst_theta = annotated_theta , sig_inst_skols = annotated_tvs })) = -- Choose quantifiers for a partial type signature - do { psig_qtvbndr_prs <- zonkTyVarTyVarPairs annotated_tvs - ; let psig_qtv_prs = mapSnd binderVar psig_qtvbndr_prs + do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs + ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs + ; let psig_qtvs = map binderVar psig_qtv_bndrs + psig_qtv_set = mkVarSet psig_qtvs + psig_qtv_prs = psig_qtv_nms `zip` psig_qtvs + -- Check whether the quantified variables of the -- partial signature have been unified together @@ -958,17 +976,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs , not (tv `elem` qtvs) ] - ; let psig_qtvbndrs = map snd psig_qtvbndr_prs - psig_qtvs = mkVarSet (map snd psig_qtv_prs) - ; annotated_theta <- zonkTcTypes annotated_theta - ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx + ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx - ; let keep_me = free_tvs `unionVarSet` psig_qtvs + ; let keep_me = free_tvs `unionVarSet` psig_qtv_set final_qtvs = [ mkTyVarBinder vis tv | tv <- qtvs -- Pulling from qtvs maintains original order , tv `elemVarSet` keep_me - , let vis = case lookupVarBndr tv psig_qtvbndrs of + , let vis = case lookupVarBndr tv psig_qtv_bndrs of Just spec -> spec Nothing -> InferredSpec ] @@ -1454,17 +1469,7 @@ tcExtendTyVarEnvFromSig sig_inst thing_inside thing_inside tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a --- Extend the TcBinderStack for the RHS of the binding, with --- the monomorphic Id. That way, if we have, say --- f = \x -> blah --- and something goes wrong in 'blah', we get a "relevant binding" --- looking like f :: alpha -> beta --- This applies if 'f' has a type signature too: --- f :: forall a. [a] -> [a] --- f x = True --- We can't unify True with [a], and a relevant binding is f :: [a] -> [a] --- If we had the *polymorphic* version of f in the TcBinderStack, it --- would not be reported as relevant, because its type is closed +-- See Note [Relevant bindings and the binder stack] tcExtendIdBinderStackForRhs infos thing_inside = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel | MBI { mbi_mono_id = mono_id } <- infos ] @@ -1480,7 +1485,22 @@ getMonoBindInfo tc_binds get_info (TcPatBind infos _ _ _) rest = infos ++ rest -{- Note [Typechecking pattern bindings] +{- Note [Relevant bindings and the binder stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When typecking a binding we extend the TcBinderStack for the RHS of +the binding, with the /monomorphic/ Id. That way, if we have, say + f = \x -> blah +and something goes wrong in 'blah', we get a "relevant binding" +looking like f :: alpha -> beta +This applies if 'f' has a type signature too: + f :: forall a. [a] -> [a] + f x = True +We can't unify True with [a], and a relevant binding is f :: [a] -> [a] +If we had the *polymorphic* version of f in the TcBinderStack, it +would not be reported as relevant, because its type is closed. +(See TcErrors.relevantBindings.) + +Note [Typechecking pattern bindings] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Look at: - typecheck/should_compile/ExPat diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs index ab5e021653..9f31d7938a 100644 --- a/compiler/GHC/Tc/Gen/Default.hs +++ b/compiler/GHC/Tc/Gen/Default.hs @@ -70,8 +70,8 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _) tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type tc_default_ty deflt_clss hs_ty - = do { (ty, _kind) <- solveEqualities $ - tcLHsType hs_ty + = do { ty <- solveEqualities $ + tcInferLHsType hs_ty ; ty <- zonkTcTypeToType ty -- establish Type invariants ; checkValidType DefaultDeclCtxt ty diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 2d6b25df10..b4c3b6275c 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -13,20 +13,15 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} --- | Typecheck an expression module GHC.Tc.Gen.Expr - ( tcCheckExpr - , tcLExpr, tcLExprNC, tcExpr - , tcInferSigma - , tcInferRho, tcInferRhoNC - , tcSyntaxOp, tcSyntaxOpGen - , SyntaxOpType(..) - , synKnownType - , tcCheckId - , addAmbiguousNameErr - , getFixedTyVars - ) -where + ( tcCheckPolyExpr, + tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC, + tcInferSigma, tcInferRho, tcInferRhoNC, + tcExpr, + tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType, + tcCheckId, + addAmbiguousNameErr, + getFixedTyVars ) where #include "HsVersions.h" @@ -101,25 +96,35 @@ import qualified Data.Set as Set ************************************************************************ -} -tcCheckExpr, tcCheckExprNC + +tcCheckPolyExpr, tcCheckPolyExprNC :: LHsExpr GhcRn -- Expression to type check -> TcSigmaType -- Expected type (could be a polytype) -> TcM (LHsExpr GhcTc) -- Generalised expr with expected type --- tcCheckExpr is a convenient place (frequent but not too frequent) +-- tcCheckPolyExpr is a convenient place (frequent but not too frequent) -- place to add context information. -- The NC version does not do so, usually because the caller wants -- to do so himself. -tcCheckExpr expr res_ty +tcCheckPolyExpr expr res_ty = tcPolyExpr expr (mkCheckExpType res_ty) +tcCheckPolyExprNC expr res_ty = tcPolyExprNC expr (mkCheckExpType res_ty) + +-- These versions take an ExpType +tcPolyExpr, tcPolyExprNC + :: LHsExpr GhcRn -> ExpSigmaType + -> TcM (LHsExpr GhcTcId) + +tcPolyExpr expr res_ty = addExprCtxt expr $ - tcCheckExprNC expr res_ty + do { traceTc "tcPolyExpr" (ppr res_ty) + ; tcPolyExprNC expr res_ty } -tcCheckExprNC (L loc expr) res_ty +tcPolyExprNC (L loc expr) res_ty = setSrcSpan loc $ - do { traceTc "tcCheckExprNC" (ppr res_ty) - ; (wrap, expr') <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty -> - tcExpr expr (mkCheckExpType res_ty) + do { traceTc "tcPolyExprNC" (ppr res_ty) + ; (wrap, expr') <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty -> + tcExpr expr res_ty ; return $ L loc (mkHsWrap wrap expr') } --------------- @@ -134,6 +139,30 @@ tcInferSigma le@(L loc expr) ; return (L loc (applyHsArgs fun args), ty) } --------------- +tcCheckMonoExpr, tcCheckMonoExprNC + :: LHsExpr GhcRn -- Expression to type check + -> TcRhoType -- Expected type + -- Definitely no foralls at the top + -> TcM (LHsExpr GhcTcId) +tcCheckMonoExpr expr res_ty = tcMonoExpr expr (mkCheckExpType res_ty) +tcCheckMonoExprNC expr res_ty = tcMonoExprNC expr (mkCheckExpType res_ty) + +tcMonoExpr, tcMonoExprNC + :: LHsExpr GhcRn -- Expression to type check + -> ExpRhoType -- Expected type + -- Definitely no foralls at the top + -> TcM (LHsExpr GhcTcId) + +tcMonoExpr expr res_ty + = addExprCtxt expr $ + tcMonoExprNC expr res_ty + +tcMonoExprNC (L loc expr) res_ty + = setSrcSpan loc $ + do { expr' <- tcExpr expr res_ty + ; return (L loc expr') } + +--------------- tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. tcInferRho le = addExprCtxt le (tcInferRhoNC le) @@ -144,15 +173,11 @@ tcInferRhoNC (L loc expr) ; return (L loc expr', rho) } -{- -************************************************************************ +{- ********************************************************************* * * tcExpr: the main expression typechecker * * -************************************************************************ - -NB: The res_ty is always deeply skolemised. --} +********************************************************************* -} tcLExpr, tcLExprNC :: LHsExpr GhcRn -- Expression to type check @@ -241,7 +266,7 @@ tcExpr e@(HsOverLabel _ mb_fromLabel l) res_ty (mkEmptyWildCardBndrs (L loc (HsTyLit noExtField (HsStrTy NoSourceText l)))) tcExpr (HsLam x match) res_ty - = do { (match', wrap) <- tcMatchLambda herald match_ctxt match res_ty + = do { (wrap, match') <- tcMatchLambda herald match_ctxt match res_ty ; return (mkHsWrap wrap (HsLam x match')) } where match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody } @@ -252,7 +277,7 @@ tcExpr (HsLam x match) res_ty text "has"] tcExpr e@(HsLamCase x matches) res_ty - = do { (matches', wrap) + = do { (wrap, matches') <- tcMatchLambda msg match_ctxt matches res_ty -- The laziness annotation is because we don't want to fail here -- if there are multiple arguments @@ -335,7 +360,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; let doc = text "The first argument of ($) takes" orig1 = lexprCtOrigin arg1 ; (wrap_arg1, [arg2_sigma], op_res_ty) <- - matchActualFunTys doc orig1 (Just (unLoc arg1)) 1 arg1_ty + matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty -- We have (arg1 $ arg2) -- So: arg1_ty = arg2_ty -> op_res_ty @@ -351,7 +376,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty (tcTypeKind 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 matchActualFunTys would fail) + -- (because otherwise matchActualFunTysRho would fail) -- So this 'unifyKind' will either succeed with Refl, or will -- produce an insoluble constraint * ~ #, which we'll report later. @@ -385,7 +410,8 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; (op', op_ty) <- tcInferRhoNC op ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_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. @@ -405,12 +431,13 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty tcExpr expr@(SectionR x op arg2) res_ty = do { (op', op_ty) <- tcInferRhoNC op ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty - ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) - (mkVisFunTy arg1_ty op_res_ty) res_ty + <- matchActualFunTysRho (mk_op_msg op) fn_orig + (Just (unLoc op)) 2 op_ty ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2 - ; return ( mkHsWrap wrap_res $ - SectionR x (mkLHsWrap wrap_fun op') arg2' ) } + ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2' + act_res_ty = mkVisFunTy arg1_ty op_res_ty + ; tcWrapResultMono expr expr' act_res_ty res_ty } + where fn_orig = lexprCtOrigin op -- It's important to use the origin of 'op', so that call-stacks @@ -424,13 +451,12 @@ tcExpr expr@(SectionL x arg1 op) res_ty | otherwise = 2 ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) - n_reqd_args op_ty - ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) - (mkVisFunTys arg_tys op_res_ty) 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 - ; return ( mkHsWrap wrap_res $ - SectionL x arg1' (mkLHsWrap wrap_fn op') ) } + ; 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 } where fn_orig = lexprCtOrigin op -- It's important to use the origin of 'op', so that call-stacks @@ -460,19 +486,19 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty ; arg_tys <- case boxity of { Boxed -> newFlexiTyVarTys arity liftedTypeKind ; Unboxed -> replicateM arity newOpenFlexiTyVarTy } - ; let actual_res_ty - = mkVisFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args] - (mkTupleTy1 boxity arg_tys) - -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make - - ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple") - (Just expr) - actual_res_ty res_ty -- Handle tuple sections where ; tup_args1 <- tcTupArgs tup_args arg_tys - ; return $ mkHsWrap wrap (ExplicitTuple x tup_args1 boxity) } + ; let expr' = ExplicitTuple x tup_args1 boxity + act_res_ty = mkVisFunTys [ty | (ty, (L _ (Missing _))) + <- arg_tys `zip` tup_args] + (mkTupleTy1 boxity arg_tys) + -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make + + ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty) + + ; tcWrapResultMono expr expr' act_res_ty res_ty } tcExpr (ExplicitSum _ alt arity expr) res_ty = do { let sum_tc = sumTyCon arity @@ -480,7 +506,7 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty ; -- Drop levity vars, we don't care about them here let arg_tys' = drop arity arg_tys - ; expr' <- tcCheckExpr expr (arg_tys' `getNth` (alt - 1)) + ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1)) ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } -- This will see the empty list only when -XOverloadedLists. @@ -502,7 +528,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty ; return (exprs', elt_ty) } ; return $ ExplicitList elt_ty (Just fln') exprs' } - where tc_elt elt_ty expr = tcCheckExpr expr elt_ty + where tc_elt elt_ty expr = tcCheckPolyExpr expr elt_ty {- ************************************************************************ @@ -527,6 +553,13 @@ tcExpr (HsCase x scrut matches) res_ty -- -- But now, in the GADT world, we need to typecheck the scrutinee -- first, to get type info that may be refined in the case alternatives + + -- Typecheck the scrutinee. We use tcInferRho but tcInferSigma + -- would also be possible (tcMatchesCase accepts sigma-types) + -- Interesting litmus test: do these two behave the same? + -- case id of {..} + -- case (\v -> v) of {..} + -- This design choice is discussed in #17790 (scrut', scrut_ty) <- tcInferRho scrut ; traceTc "HsCase" (ppr scrut_ty) @@ -550,9 +583,9 @@ tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty = do { ((pred', b1', b2'), fun') <- tcSyntaxOp IfOrigin fun [SynAny, SynAny, SynAny] res_ty $ \ [pred_ty, b1_ty, b2_ty] -> - do { pred' <- tcCheckExpr pred pred_ty - ; b1' <- tcCheckExpr b1 b1_ty - ; b2' <- tcCheckExpr b2 b2_ty + do { pred' <- tcCheckPolyExpr pred pred_ty + ; b1' <- tcCheckPolyExpr b1 b1_ty + ; b2' <- tcCheckPolyExpr b2 b2_ty ; return (pred', b1', b2') } ; return (HsIf x fun' pred' b1' b2') } @@ -591,7 +624,7 @@ tcExpr (HsStatic fvs expr) res_ty addErrCtxt (hang (text "In the body of a static form:") 2 (ppr expr) ) $ - tcCheckExprNC expr expr_ty + tcCheckPolyExprNC expr expr_ty -- Check that the free variables of the static form are closed. -- It's OK to use nonDetEltsUniqSet here as the only side effects of @@ -637,25 +670,26 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name ; checkMissingFields con_like rbinds ; (con_expr, con_sigma) <- tcInferId con_name - ; (con_wrap, con_tau) <- - topInstantiate (OccurrenceOf con_name) con_sigma + ; (con_wrap, con_tau) <- topInstantiate orig con_sigma -- a shallow instantiation should really be enough for -- a data constructor. ; let arity = conLikeArity con_like Right (arg_tys, actual_res_ty) = tcSplitFunTysN arity con_tau - ; case conLikeWrapId_maybe con_like of - Nothing -> nonBidirectionalErr (conLikeName con_like) - Just con_id -> do { - res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon") - (Just expr) actual_res_ty res_ty - ; rbinds' <- tcRecordBinds con_like arg_tys rbinds - ; return $ - mkHsWrap res_wrap $ - RecordCon { rcon_ext = RecordConTc - { rcon_con_like = con_like - , rcon_con_expr = mkHsWrap con_wrap con_expr } - , rcon_con_name = L loc con_id - , rcon_flds = rbinds' } } } + ; case conLikeWrapId_maybe con_like of { + Nothing -> nonBidirectionalErr (conLikeName con_like) ; + Just con_id -> + + do { rbinds' <- tcRecordBinds con_like arg_tys rbinds + ; let rcon_tc = RecordConTc + { rcon_con_like = con_like + , rcon_con_expr = mkHsWrap con_wrap con_expr } + expr' = RecordCon { rcon_ext = rcon_tc + , rcon_con_name = L loc con_id + , rcon_flds = rbinds' } + + ; tcWrapResultMono expr expr' actual_res_ty res_ty } } } + where + orig = OccurrenceOf con_name {- Note [Type of a record update] @@ -906,8 +940,6 @@ 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 - ; wrap_res <- tcSubTypeHR (exprCtOrigin expr) - (Just expr) rec_res_ty res_ty ; co_scrut <- unifyType (Just (unLoc 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 @@ -937,16 +969,16 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta' -- Phew! - ; return $ - mkHsWrap wrap_res $ - RecordUpd { rupd_expr - = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr') - , rupd_flds = rbinds' - , rupd_ext = RecordUpdTc - { rupd_cons = relevant_cons - , rupd_in_tys = scrut_inst_tys - , rupd_out_tys = result_inst_tys - , rupd_wrap = req_wrap }} } + ; let upd_tc = RecordUpdTc { rupd_cons = relevant_cons + , rupd_in_tys = scrut_inst_tys + , rupd_out_tys = result_inst_tys + , rupd_wrap = req_wrap } + expr' = RecordUpd { rupd_expr = mkLHsWrap fam_co $ + mkLHsWrapCo co_scrut record_expr' + , rupd_flds = rbinds' + , rupd_ext = upd_tc } + + ; tcWrapResult expr expr' rec_res_ty res_ty } tcExpr e@(HsRecFld _ f) res_ty = tcCheckRecSelId e f res_ty @@ -1038,7 +1070,7 @@ tcArithSeq :: Maybe (SyntaxExpr GhcRn) -> ArithSeqInfo GhcRn -> ExpRhoType tcArithSeq witness seq@(From expr) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr' <- tcCheckExpr expr elt_ty + ; expr' <- tcCheckPolyExpr expr elt_ty ; enum_from <- newMethodFromName (ArithSeqOrigin seq) enumFromName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1046,8 +1078,8 @@ tcArithSeq witness seq@(From expr) res_ty tcArithSeq witness seq@(FromThen expr1 expr2) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) enumFromThenName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1055,8 +1087,8 @@ tcArithSeq witness seq@(FromThen expr1 expr2) res_ty tcArithSeq witness seq@(FromTo expr1 expr2) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) enumFromToName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1064,9 +1096,9 @@ tcArithSeq witness seq@(FromTo expr1 expr2) res_ty tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty - ; expr3' <- tcCheckExpr expr3 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty + ; expr3' <- tcCheckPolyExpr expr3 elt_ty ; eft <- newMethodFromName (ArithSeqOrigin seq) enumFromThenToName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1251,13 +1283,11 @@ tcInferApp expr 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) } @@ -1364,9 +1394,9 @@ tcArgs fun orig_fun_ty orig_args _ -> ty_app_err upsilon_ty hs_ty_arg } go n so_far fun_ty (HsEValArg loc arg : args) - = do { (wrap, [arg_ty], res_ty) - <- matchActualFunTysPart herald fun_orig (Just fun) - n_val_args so_far 1 fun_ty + = 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' @@ -1465,13 +1495,12 @@ tcArg :: HsExpr GhcRn -- The function (for error messages) -> Int -- # of argument -> TcM (LHsExpr GhcTc) -- Resulting argument tcArg fun arg ty arg_no - = addErrCtxt (funAppCtxt fun arg arg_no) $ - do { traceTc "tcArg {" $ - vcat [ text "arg #" <> ppr arg_no <+> dcolon <+> ppr ty - , text "arg:" <+> ppr arg ] - ; arg' <- tcCheckExprNC arg ty - ; traceTc "tcArg }" empty - ; return arg' } + = 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 ] + ; tcCheckPolyExprNC arg ty } ---------------- tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc] @@ -1479,7 +1508,7 @@ tcTupArgs args tys = ASSERT( equalLength args tys ) mapM go (args `zip` tys) where go (L l (Missing {}), arg_ty) = return (L l (Missing arg_ty)) - go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckExpr expr arg_ty + go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty ; return (L l (Present x expr')) } --------------------------- @@ -1536,7 +1565,7 @@ tcSynArgE :: CtOrigin -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) tcSynArgE orig sigma_ty syn_ty thing_inside = do { (skol_wrap, (result, ty_wrapper)) - <- tcSkolemise GenSigCtxt sigma_ty $ \ _ rho_ty -> + <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty -> go rho_ty syn_ty ; return (result, skol_wrap <.> ty_wrapper) } where @@ -1554,11 +1583,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside ; return (result, mkWpCastN list_co) } go rho_ty (SynFun arg_shape res_shape) - = do { ( ( ( (result, arg_ty, res_ty) - , res_wrapper ) -- :: res_ty_out "->" res_ty - , arg_wrapper1, [], arg_wrapper2 ) -- :: arg_ty "->" arg_ty_out - , match_wrapper ) -- :: (arg_ty -> res_ty) "->" rho_ty - <- matchExpectedFunTys herald 1 (mkCheckExpType rho_ty) $ + = do { ( match_wrapper -- :: (arg_ty -> res_ty) "->" rho_ty + , ( ( (result, arg_ty, res_ty) + , res_wrapper ) -- :: res_ty_out "->" res_ty + , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out + <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $ \ [arg_ty] res_ty -> do { arg_tc_ty <- expTypeToType arg_ty ; res_tc_ty <- expTypeToType res_ty @@ -1604,7 +1633,8 @@ tcSynArgA :: CtOrigin -- and a wrapper to be applied to the overall expression tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside = do { (match_wrapper, arg_tys, res_ty) - <- matchActualFunTys herald orig Nothing (length arg_shapes) sigma_ty + <- matchActualFunTysRho herald orig Nothing + (length arg_shapes) sigma_ty -- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty) ; ((result, res_wrapper), arg_wrappers) <- tc_syn_args_e arg_tys arg_shapes $ \ arg_results -> @@ -1634,7 +1664,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside = do { result <- thing_inside [res_ty] ; return (result, idHsWrapper) } tc_syn_arg res_ty SynRho thing_inside - = do { (inst_wrap, rho_ty) <- deeplyInstantiate orig res_ty + = do { (inst_wrap, rho_ty) <- topInstantiate orig res_ty -- inst_wrap :: res_ty "->" rho_ty ; result <- thing_inside [rho_ty] ; return (result, inst_wrap) } @@ -1648,7 +1678,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside tc_syn_arg _ (SynFun {}) _ = pprPanic "tcSynArgA hits a SynFun" (ppr orig) tc_syn_arg res_ty (SynType the_ty) thing_inside - = do { wrap <- tcSubTypeO orig GenSigCtxt res_ty the_ty + = do { wrap <- tcSubType orig GenSigCtxt res_ty the_ty ; result <- thing_inside [] ; return (result, wrap) } @@ -1687,22 +1717,10 @@ in the other order, the extra signature in f2 is reqd. 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 { (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id - ; given <- newEvVars theta - ; traceTc "tcExprSig: CompleteSig" $ - vcat [ text "poly_id:" <+> ppr poly_id <+> dcolon <+> ppr (idType poly_id) - , text "tv_prs:" <+> ppr tv_prs ] - - ; let skol_info = SigSkol ExprSigCtxt (idType poly_id) tv_prs - skol_tvs = map snd tv_prs - ; (ev_binds, expr') <- checkConstraints skol_info skol_tvs given $ - tcExtendNameTyVarEnv tv_prs $ - tcCheckExprNC expr tau - - ; let poly_wrap = mkWpTyLams skol_tvs - <.> mkWpLams given - <.> mkWpLet ev_binds - ; return (mkLHsWrap poly_wrap expr', idType poly_id) } + 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 @@ -1711,7 +1729,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) do { sig_inst <- tcInstSig sig ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $ tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $ - tcCheckExprNC expr (sig_inst_tau 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 @@ -1735,7 +1753,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) 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 tcSubType_NC ExprSigCtxt inferred_sigma my_sigma + else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) ; let poly_wrap = wrap @@ -2476,7 +2494,7 @@ tcRecordField :: ConLike -> Assoc Name Type tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs | Just field_ty <- assocMaybe flds_w_tys sel_name = addErrCtxt (fieldCtxt field_lbl) $ - do { rhs' <- tcCheckExprNC rhs field_ty + do { rhs' <- tcCheckPolyExprNC rhs field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) field_ty loc @@ -2584,7 +2602,7 @@ addFunResCtxt has_args fun fun_res_ty env_ty -- function types] (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res' -- No need to call tcSplitNestedSigmaTys here, since env_ty is - -- an ExpRhoTy, i.e., it's already deeply instantiated. + -- 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 diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot index d9138a4d7e..1f26ef242a 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs-boot +++ b/compiler/GHC/Tc/Gen/Expr.hs-boot @@ -6,16 +6,26 @@ import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Origin ( CtOrigin ) import GHC.Hs.Extension ( GhcRn, GhcTcId ) -tcCheckExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId) - -tcLExpr, tcLExprNC - :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId) -tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId) - -tcInferRho, tcInferRhoNC - :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcRhoType) - -tcInferSigma :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcSigmaType) +tcCheckPolyExpr :: + LHsExpr GhcRn + -> TcSigmaType + -> TcM (LHsExpr GhcTcId) + +tcMonoExpr, tcMonoExprNC :: + LHsExpr GhcRn + -> ExpRhoType + -> TcM (LHsExpr GhcTcId) +tcCheckMonoExpr, tcCheckMonoExprNC :: + LHsExpr GhcRn + -> TcRhoType + -> TcM (LHsExpr GhcTcId) + +tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId) + +tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType) + +tcInferRho, tcInferRhoNC :: + LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcRhoType) tcSyntaxOp :: CtOrigin -> SyntaxExprRn diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs index 8163e6820d..06febcef33 100644 --- a/compiler/GHC/Tc/Gen/Foreign.hs +++ b/compiler/GHC/Tc/Gen/Foreign.hs @@ -388,7 +388,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe = addErrCtxt (foreignDeclCtxt fo) $ do sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty - rhs <- tcCheckExpr (nlHsVar nm) sig_ty + rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index cdbaab115b..1cd4e27c8d 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -31,8 +31,8 @@ module GHC.Tc.Gen.HsType ( bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol, ContextKind(..), - -- Type checking type and class decls - bindTyClTyVars, + -- Type checking type and class decls, and instances thereof + bindTyClTyVars, tcFamTyPats, etaExpandAlgTyCon, tcbVisibilities, -- tyvars @@ -46,13 +46,11 @@ module GHC.Tc.Gen.HsType ( tcNamedWildCardBinders, tcHsLiftedType, tcHsOpenType, tcHsLiftedTypeNC, tcHsOpenTypeNC, - tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType, - tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps, + tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType, + tcHsMbContext, tcHsContext, tcLHsPredType, failIfEmitsConstraints, solveEqualities, -- useful re-export - typeLevelMode, kindLevelMode, - kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone, -- Sort-checking kinds @@ -115,6 +113,7 @@ import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt import GHC.Data.Maybe +import GHC.Data.Bag( unitBag ) import Data.List ( find ) import Control.Monad @@ -159,6 +158,91 @@ checking until step (3). Check types AND do validity checking * * ************************************************************************ + +Note [Keeping implicitly quantified variables in order] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When the user implicitly quantifies over variables (say, in a type +signature), we need to come up with some ordering on these variables. +This is done by bumping the TcLevel, bringing the tyvars into scope, +and then type-checking the thing_inside. The constraints are all +wrapped in an implication, which is then solved. Finally, we can +zonk all the binders and then order them with scopedSort. + +It's critical to solve before zonking and ordering in order to uncover +any unifications. You might worry that this eager solving could cause +trouble elsewhere. I don't think it will. Because it will solve only +in an increased TcLevel, it can't unify anything that was mentioned +elsewhere. Additionally, we require that the order of implicitly +quantified variables is manifest by the scope of these variables, so +we're not going to learn more information later that will help order +these variables. + +Note [Recipe for checking a signature] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Checking a user-written signature requires several steps: + + 1. Generate constraints. + 2. Solve constraints. + 3. Promote tyvars and/or kind-generalize. + 4. Zonk. + 5. Check validity. + +There may be some surprises in here: + +Step 2 is necessary for two reasons: most signatures also bring +implicitly quantified variables into scope, and solving is necessary +to get these in the right order (see Note [Keeping implicitly +quantified variables in order]). Additionally, solving is necessary in +order to kind-generalize correctly: otherwise, we do not know which +metavariables are left unsolved. + +Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to +kindGeneralize{All,Some,None}. Here, we have to deal with the fact that +metatyvars generated in the type may have a bumped TcLevel, because explicit +foralls raise the TcLevel. To avoid these variables from ever being visible in +the surrounding context, we must obey the following dictum: + + Every metavariable in a type must either be + (A) generalized, or + (B) promoted, or See Note [Promotion in signatures] + (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType + +The kindGeneralize functions do not require pre-zonking; they zonk as they +go. + +If you are actually doing kind-generalization, you need to bump the level +before generating constraints, as we will only generalize variables with +a TcLevel higher than the ambient one. + +After promoting/generalizing, we need to zonk again because both +promoting and generalizing fill in metavariables. + +Note [Promotion in signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If an unsolved metavariable in a signature is not generalized +(because we're not generalizing the construct -- e.g., pattern +sig -- or because the metavars are constrained -- see kindGeneralizeSome) +we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables] +in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing +and the reinstantiating with a fresh metavariable at the current level. +So in some sense, we generalize *all* variables, but then re-instantiate +some of them. + +Here is an example of why we must promote: + foo (x :: forall a. a -> Proxy b) = ... + +In the pattern signature, `b` is unbound, and will thus be brought into +scope. We do not know its kind: it will be assigned kappa[2]. Note that +kappa is at TcLevel 2, because it is invented under a forall. (A priori, +the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel +than the surrounding context.) This kappa cannot be solved for while checking +the pattern signature (which is not kind-generalized). When we are checking +the *body* of foo, though, we need to unify the type of x with the argument +type of bar. At this point, the ambient TcLevel is 1, and spotting a +matavariable with level 2 would violate the (WantedTvInv) invariant of +Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing, +we promote the metavariable to level 1. This is all done in kindGeneralizeNone. + -} funsSigCtxt :: [Located Name] -> UserTypeCtxt @@ -213,19 +297,21 @@ kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars <- pushTcLevelM $ solveLocalEqualitiesX "kcClassSigType" $ bindImplicitTKBndrs_Skol sig_vars $ - tc_lhs_type typeLevelMode hs_ty liftedTypeKind + tcLHsType hs_ty liftedTypeKind - ; emitResidualTvConstraint skol_info Nothing spec_tkvs - tc_lvl wanted } + ; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted } tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type -- Does not do validity checking tcClassSigType skol_info names sig_ty = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $ - snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind) + do { (implic, ty) <- tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind) + ; emitImplication implic + ; return ty } -- Do not zonk-to-Type, nor perform a validity check -- We are in a knot with the class and associated types -- Zonking and validity checking is done by tcClassDecl + -- -- No need to fail here if the type has an error: -- If we're in the kind-checking phase, the solveEqualities -- in kcTyClGroup catches the error @@ -247,46 +333,36 @@ tcHsSigType ctxt sig_ty do { traceTc "tcHsSigType {" (ppr sig_ty) -- Generalise here: see Note [Kind generalisation] - ; (insol, ty) <- tc_hs_sig_type skol_info sig_ty - (expectedKindInCtxt ctxt) - ; ty <- zonkTcType ty + ; (implic, ty) <- tc_hs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt) - ; when insol failM - -- See Note [Fail fast if there are insoluble kind equalities] in GHC.Tc.Solver + -- Spit out the implication (and perhaps fail fast) + -- See Note [Failure in local type signatures] in GHC.Tc.Solver + ; emitFlatConstraints (mkImplicWC (unitBag implic)) + ; ty <- zonkTcType ty ; checkValidType ctxt ty ; traceTc "end tcHsSigType }" (ppr ty) ; return ty } where skol_info = SigTypeSkol ctxt --- Does validity checking and zonking. -tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind) -tcStandaloneKindSig (L _ kisig) = case kisig of - StandaloneKindSig _ (L _ name) ksig -> - let ctxt = StandaloneKindSigCtxt name in - addSigCtxt ctxt (hsSigType ksig) $ - do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt) - ; checkValidType ctxt kind - ; return (name, kind) } - tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn - -> ContextKind -> TcM (Bool, TcType) + -> ContextKind -> TcM (Implication, TcType) -- Kind-checks/desugars an 'LHsSigType', -- solve equalities, -- and then kind-generalizes. -- This will never emit constraints, as it uses solveEqualities internally. -- No validity checking or zonking --- Returns also a Bool indicating whether the type induced an insoluble constraint; --- True <=> constraint is insoluble +-- Returns also an implication for the unsolved constraints tc_hs_sig_type skol_info hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { (tc_lvl, (wanted, (spec_tkvs, ty))) <- pushTcLevelM $ solveLocalEqualitiesX "tc_hs_sig_type" $ + -- See Note [Failure in local type signatures] bindImplicitTKBndrs_Skol sig_vars $ do { kind <- newExpectedKind ctxt_kind - ; tc_lhs_type typeLevelMode hs_ty kind } + ; tcLHsType hs_ty kind } -- Any remaining variables (unsolved in the solveLocalEqualities) -- should be in the global tyvars, and therefore won't be quantified @@ -301,18 +377,67 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind ; let should_gen = not . (`elemVarSet` constrained) ; kvs <- kindGeneralizeSome should_gen ty1 - ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs) - tc_lvl wanted - ; return (insolubleWC wanted, mkInfForAllTys kvs ty1) } + -- Build an implication for any as-yet-unsolved kind equalities + -- See Note [Skolem escape in type signatures] + ; implic <- buildTvImplication skol_info (kvs ++ spec_tkvs) tc_lvl wanted + + ; return (implic, mkInfForAllTys kvs ty1) } + +{- Note [Skolem escape in type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tcHsSigType is tricky. Consider (T11142) + foo :: forall b. (forall k (a :: k). SameKind a b) -> () +This is ill-kinded becuase of a nested skolem-escape. + +That will show up as an un-solvable constraint in the implication +returned by buildTvImplication in tc_hs_sig_type. See Note [Skolem +escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable +(the unification variable for b's kind is untouchable). + +Then, in GHC.Tc.Solver.emitFlatConstraints (called from tcHsSigType) +we'll try to float out the constraint, be unable to do so, and fail. +See GHC.Tc.Solver Note [Failure in local type signatures] for more +detail on this. + +The separation between tcHsSigType and tc_hs_sig_type is because +tcClassSigType wants to use the latter, but *not* fail fast, because +there are skolems from the class decl which are in scope; but it's fine +not to because tcClassDecl1 has a solveEqualities wrapped around all +the tcClassSigType calls. + +That's why tcHsSigType does emitFlatConstraints (which fails fast) but +tcClassSigType just does emitImplication (which does not). Ugh. + +c.f. see also Note [Skolem escape and forall-types]. The difference +is that we don't need to simplify at a forall type, only at the +top level of a signature. +-} + +-- Does validity checking and zonking. +tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind) +tcStandaloneKindSig (L _ kisig) = case kisig of + StandaloneKindSig _ (L _ name) ksig -> + let ctxt = StandaloneKindSigCtxt name in + addSigCtxt ctxt (hsSigType ksig) $ + do { let mode = mkMode KindLevel + ; kind <- tc_top_lhs_type mode ksig (expectedKindInCtxt ctxt) + ; checkValidType ctxt kind + ; return (name, kind) } + -tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type +tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type +tcTopLHsType hs_ty ctxt_kind + = tc_top_lhs_type (mkMode TypeLevel) hs_ty ctxt_kind + +tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type -- tcTopLHsType is used for kind-checking top-level HsType where -- we want to fully solve /all/ equalities, and report errors -- Does zonking, but not validity checking because it's used -- for things (like deriving and instances) that aren't -- ordinary types -tcTopLHsType mode hs_sig_type ctxt_kind +-- Used for both types and kinds +tc_top_lhs_type mode hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { traceTc "tcTopLHsType {" (ppr hs_ty) ; (spec_tkvs, ty) @@ -340,7 +465,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind]) tcHsDeriv hs_ty = do { ty <- checkNoErrs $ -- Avoid redundant error report -- with "illegal deriving", below - tcTopLHsType typeLevelMode hs_ty AnyKind + tcTopLHsType hs_ty AnyKind ; let (tvs, pred) = splitForAllTys ty (kind_args, _) = splitFunTys (tcTypeKind pred) ; case getClassPredTys_maybe pred of @@ -369,7 +494,7 @@ tcDerivStrategy mb_lds tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy tc_deriv_strategy (ViaStrategy ty) = do - ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind + ty' <- checkNoErrs $ tcTopLHsType ty AnyKind let (via_tvs, via_pred) = splitForAllTys ty' pure (ViaStrategy via_pred, via_tvs) @@ -387,7 +512,7 @@ tcHsClsInstType user_ctxt hs_inst_ty -- eagerly avoids follow-on errors when checkValidInstance -- sees an unsolved coercion hole inst_ty <- checkNoErrs $ - tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind) + tcTopLHsType hs_inst_ty (TheKind constraintKind) ; checkValidInstance user_ctxt hs_inst_ty inst_ty ; return inst_ty } @@ -397,14 +522,15 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType tcHsTypeApp wc_ty kind | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty - = do { ty <- solveLocalEqualities "tcHsTypeApp" $ + = do { mode <- mkHoleMode TypeLevel HM_VTA + -- HM_VTA: See Note [Wildcards in visible type application] + ; ty <- addTypeCtxt hs_ty $ + solveLocalEqualities "tcHsTypeApp" $ -- We are looking at a user-written type, very like a -- signature so we want to solve its equalities right now - unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- See Note [Wildcards in visible type application] tcNamedWildCardBinders sig_wcs $ \ _ -> - tcCheckLHsType hs_ty (TheKind kind) + tc_lhs_type mode hs_ty kind + -- We do not kind-generalize type applications: we just -- instantiate with exactly what the user says. -- See Note [No generalization in type application] @@ -448,6 +574,31 @@ There is also the possibility of mentioning a wildcard -} +tcFamTyPats :: TyCon + -> HsTyPats GhcRn -- Patterns + -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind) +-- Check the LHS of a type/data family instance +-- e.g. type instance F ty1 .. tyn = ... +-- Used for both type and data families +tcFamTyPats fam_tc hs_pats + = do { traceTc "tcFamTyPats {" $ + vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ] + + ; mode <- mkHoleMode TypeLevel HM_FamPat + -- HM_FamPat: See Note [Wildcards in family instances] in + -- GHC.Rename.Module + ; let fun_ty = mkTyConApp fam_tc [] + ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats + + ; traceTc "End tcFamTyPats }" $ + vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] + + ; return (fam_app, res_kind) } + where + fam_name = tyConName fam_tc + fam_arity = tyConArity fam_tc + lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) + {- ************************************************************************ * * @@ -465,38 +616,38 @@ tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind - ; tc_lhs_type typeLevelMode ty ek } -tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind + ; tcLHsType ty ek } +tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind -- Like tcHsType, but takes an expected kind tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType tcCheckLHsType hs_ty exp_kind = addTypeCtxt hs_ty $ do { ek <- newExpectedKind exp_kind - ; tc_lhs_type typeLevelMode hs_ty ek } + ; tcLHsType hs_ty ek } -tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind) +tcInferLHsType :: LHsType GhcRn -> TcM TcType -- Called from outside: set the context -tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty) - --- Like tcLHsType, but use it in a context where type synonyms and type families --- do not need to be saturated, like in a GHCi :kind call -tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind) -tcLHsTypeUnsaturated hs_ty - | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty) +tcInferLHsType hs_ty = addTypeCtxt hs_ty $ - do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty - ; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args } - -- Notice the 'nosat'; do not instantiate trailing - -- invisible arguments of a type family. - -- See Note [Dealing with :kind] + do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty + ; return ty } - | otherwise +-- Used to check the argument of GHCi :kind +-- Allow and report wildcards, e.g. :kind T _ +-- Do not saturate family applications: see Note [Dealing with :kind] +tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind) +tcInferLHsTypeUnsaturated hs_ty = addTypeCtxt hs_ty $ - tc_infer_lhs_type mode hs_ty - - where - mode = typeLevelMode + do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes + ; case splitHsAppTys (unLoc hs_ty) of + Just (hs_fun_ty, hs_args) + -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty + ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args } + -- Notice the 'nosat'; do not instantiate trailing + -- invisible arguments of a type family. + -- See Note [Dealing with :kind] + Nothing -> tc_infer_lhs_type mode hs_ty } {- Note [Dealing with :kind] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -507,7 +658,7 @@ Consider this GHCi command We will only get the 'forall' if we /refrain/ from saturating those invisible binders. But generally we /do/ saturate those invisible -binders (see tcInferApps), and we want to do so for nested application +binders (see tcInferTyApps), and we want to do so for nested application even in GHCi. Consider for example (#16287) ghci> type family F :: k ghci> data T :: (forall k. k) -> Type @@ -515,7 +666,7 @@ even in GHCi. Consider for example (#16287) We want to reject this. It's just at the very top level that we want to switch off saturation. -So tcLHsTypeUnsaturated does a little special case for top level +So tcInferLHsTypeUnsaturated does a little special case for top level applications. Actually the common case is a bare variable, as above. @@ -538,21 +689,46 @@ concern things that the renamer can't handle. -- grow, at least to include the distinction between patterns and -- not-patterns. -- --- To find out where the mode is used, search for 'mode_level' -data TcTyMode = TcTyMode { mode_level :: TypeOrKind } - -typeLevelMode :: TcTyMode -typeLevelMode = TcTyMode { mode_level = TypeLevel } - -kindLevelMode :: TcTyMode -kindLevelMode = TcTyMode { mode_level = KindLevel } +-- To find out where the mode is used, search for 'mode_tyki' +-- +-- This data type is purely local, not exported from this module +data TcTyMode + = TcTyMode { mode_tyki :: TypeOrKind + + -- See Note [Levels for wildcards] + -- Nothing <=> no wildcards expected + , mode_holes :: Maybe (TcLevel, HoleMode) + } + +-- HoleMode says how to treat the occurrences +-- of anonymous wildcards; see tcAnonWildCardOcc +data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int + | HM_FamPat -- Family instances: F _ Int = Bool + | HM_VTA -- Visible type and kind application: + -- f @(Maybe _) + -- Maybe @(_ -> _) + +mkMode :: TypeOrKind -> TcTyMode +mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing } + +mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode +mkHoleMode tyki hm + = do { lvl <- getTcLevel + ; return (TcTyMode { mode_tyki = tyki + , mode_holes = Just (lvl,hm) }) } --- switch to kind level kindLevel :: TcTyMode -> TcTyMode -kindLevel mode = mode { mode_level = KindLevel } +kindLevel mode = mode { mode_tyki = KindLevel } + +instance Outputable HoleMode where + ppr HM_Sig = text "HM_Sig" + ppr HM_FamPat = text "HM_FamPat" + ppr HM_VTA = text "HM_VTA" instance Outputable TcTyMode where - ppr = ppr . mode_level + ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm }) + = text "TcTyMode" <+> braces (sep [ ppr tyki <> comma + , ppr hm ]) {- Note [Bidirectional type checking] @@ -627,11 +803,12 @@ tc_infer_hs_type mode (HsParTy _ t) tc_infer_hs_type mode ty | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty - = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty - ; tcInferApps mode hs_fun_ty fun_ty hs_args } + = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty + ; tcInferTyApps mode hs_fun_ty fun_ty hs_args } tc_infer_hs_type mode (HsKindSig _ ty sig) - = do { sig' <- tcLHsKindSig KindSigCtxt sig + = do { let mode' = mode { mode_tyki = KindLevel } + ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig -- We must typecheck the kind signature, and solve all -- its equalities etc; from this point on we may do -- things like instantiate its foralls, so it needs @@ -665,6 +842,10 @@ tc_infer_hs_type mode other_ty ; return (ty', kv) } ------------------------------------------ +tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType +tcLHsType hs_ty exp_kind + = tc_lhs_type (mkMode TypeLevel) hs_ty exp_kind + tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType tc_lhs_type mode (L span ty) exp_kind = setSrcSpan span $ @@ -718,18 +899,25 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs , hst_body = ty }) exp_kind = do { (tclvl, wanted, (inv_tv_bndrs, ty')) - <- pushLevelAndCaptureConstraints $ - bindExplicitTKBndrs_Skol hs_tvs $ + <- pushLevelAndCaptureConstraints $ + bindExplicitTKBndrs_Skol_M mode hs_tvs $ + -- The _M variant passes on the mode from the type, to + -- any wildards in kind signatures on the forall'd variables + -- e.g. f :: _ -> Int -> forall (a :: _). blah tc_lhs_type mode ty exp_kind - -- Do not kind-generalise here! See Note [Kind generalisation] - -- Why exp_kind? See Note [Body kind of HsForAllTy] - ; let skol_info = ForAllSkol (ppr forall) - m_telescope = Just (sep (map ppr hs_tvs)) + -- Why exp_kind? See Note [Body kind of HsForAllTy] - ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs + -- Do not kind-generalise here! See Note [Kind generalisation] - ; emitResidualTvConstraint skol_info m_telescope (binderVars tv_bndrs) tclvl wanted + ; let skol_info = ForAllSkol (ppr forall) (sep (map ppr hs_tvs)) + skol_tvs = binderVars inv_tv_bndrs + ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted + ; emitImplication implic + -- /Always/ emit this implication even if wanted is empty + -- We need the implication so that we check for a bad telescope + -- See Note [Skolem escape and forall-types] + ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs ; return (mkForAllTys tv_bndrs ty') } where construct_bndr :: TcInvisTVBinder -> TcM TcTyVarBinder @@ -846,7 +1034,7 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind --------- Constraint types tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind - = do { MASSERT( isTypeLevel (mode_level mode) ) + = do { MASSERT( isTypeLevel (mode_tyki mode) ) ; ty' <- tc_lhs_type mode ty liftedTypeKind ; let n' = mkStrLitTy $ hsIPNameFS n ; ipClass <- tcLookupClass ipClassName @@ -875,7 +1063,7 @@ tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek -tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek +tc_hs_type mode ty@(HsWildCardTy _) ek = tcAnonWildCardOcc mode ty ek {- Note [Variable Specificity and Forall Visibility] @@ -903,7 +1091,7 @@ Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. ------------------------------------------ tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind -> TcM TcType -tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of +tc_fun_type mode ty1 ty2 exp_kind = case mode_tyki mode of TypeLevel -> do { arg_k <- newOpenTypeKind ; res_k <- newOpenTypeKind @@ -917,46 +1105,10 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2') liftedTypeKind exp_kind } ---------------------------- -tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType -tcAnonWildCardOcc wc exp_kind - = do { wc_tv <- newWildTyVar -- The wildcard's kind will be an un-filled-in meta tyvar - - ; part_tysig <- xoptM LangExt.PartialTypeSignatures - ; warning <- woptM Opt_WarnPartialTypeSignatures - - ; unless (part_tysig && not warning) $ - emitAnonTypeHole wc_tv - -- Why the 'unless' guard? - -- See Note [Wildcards in visible kind application] - - ; checkExpectedKind wc (mkTyVarTy wc_tv) - (tyVarKind wc_tv) exp_kind } - -{- Note [Wildcards in visible kind application] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -There are cases where users might want to pass in a wildcard as a visible kind -argument, for instance: - -data T :: forall k1 k2. k1 → k2 → Type where - MkT :: T a b -x :: T @_ @Nat False n -x = MkT - -So we should allow '@_' without emitting any hole constraints, and -regardless of whether PartialTypeSignatures is enabled or not. But how would -the typechecker know which '_' is being used in VKA and which is not when it -calls emitNamedTypeHole in tcHsPartialSigType on all HsWildCardBndrs? -The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs, -but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc. -And whenever we see a '@', we automatically turn on PartialTypeSignatures and -turn off hole constraint warnings, and do not call emitAnonTypeHole -under these conditions. -See related Note [Wildcards in visible type application] here and -Note [The wildcard story for types] in GHC.Hs.Type +{- Note [Skolem escape and forall-types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Checking telescopes]. -Note [Skolem escape and forall-types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> () @@ -970,11 +1122,19 @@ unification variable, because it would be untouchable inside this inner implication. That's what the pushLevelAndCaptureConstraints, plus subsequent -emitResidualTvConstraint is all about, when kind-checking +buildTvImplication/emitImplication is all about, when kind-checking HsForAllTy. -Note that we don't need to /simplify/ the constraints here -because we aren't generalising. We just capture them. +Note that + +* We don't need to /simplify/ the constraints here + because we aren't generalising. We just capture them. + +* We can't use emitResidualTvConstraint, because that has a fast-path + for empty constraints. We can't take that fast path here, because + we must do the bad-telescope check even if there are no inner wanted + constraints. See Note [Checking telescopes] in + GHC.Tc.Types.Constraint. Lacking this check led to #16247. -} {- ********************************************************************* @@ -1117,14 +1277,14 @@ splitHsAppTys hs_ty go f as = (f, as) --------------------------- -tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind) +tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind) -- Version of tc_infer_lhs_type specialised for the head of an -- application. In particular, for a HsTyVar (which includes type --- constructors, it does not zoom off into tcInferApps and family +-- constructors, it does not zoom off into tcInferTyApps and family -- saturation -tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv))) +tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv))) = tcTyVar mode tv -tcInferAppHead mode ty +tcInferTyAppHead mode ty = tc_infer_lhs_type mode ty --------------------------- @@ -1135,24 +1295,24 @@ tcInferAppHead mode ty -- These kinds should be used to instantiate invisible kind variables; -- they come from an enclosing class for an associated type/data family. -- --- tcInferApps also arranges to saturate any trailing invisible arguments +-- tcInferTyApps also arranges to saturate any trailing invisible arguments -- of a type-family application, which is usually the right thing to do --- tcInferApps_nosat does not do this saturation; it is used only +-- tcInferTyApps_nosat does not do this saturation; it is used only -- by ":kind" in GHCi -tcInferApps, tcInferApps_nosat +tcInferTyApps, tcInferTyApps_nosat :: TcTyMode -> LHsType GhcRn -- ^ Function (for printing only) -> TcType -- ^ Function -> [LHsTypeArg GhcRn] -- ^ Args -> TcM (TcType, TcKind) -- ^ (f args, args, result kind) -tcInferApps mode hs_ty fun hs_args - = do { (f_args, res_k) <- tcInferApps_nosat mode hs_ty fun hs_args +tcInferTyApps mode hs_ty fun hs_args + = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args ; saturateFamApp f_args res_k } -tcInferApps_nosat mode orig_hs_ty fun orig_hs_args - = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args) +tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args + = do { traceTc "tcInferTyApps {" (ppr orig_hs_ty $$ ppr orig_hs_args) ; (f_args, res_k) <- go_init 1 fun orig_hs_args - ; traceTc "tcInferApps }" (ppr f_args <+> dcolon <+> ppr res_k) + ; traceTc "tcInferTyApps }" (ppr f_args <+> dcolon <+> ppr res_k) ; return (f_args, res_k) } where @@ -1205,21 +1365,18 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args Anon InvisArg _ -> instantiate ki_binder inner_ki Named (Bndr _ Specified) -> -- Visible kind application - do { traceTc "tcInferApps (vis kind app)" + do { traceTc "tcInferTyApps (vis kind app)" (vcat [ ppr ki_binder, ppr hs_ki_arg , ppr (tyBinderType ki_binder) , ppr subst ]) ; let exp_kind = substTy subst $ tyBinderType ki_binder - + ; arg_mode <- mkHoleMode KindLevel HM_VTA + -- HM_VKA: see Note [Wildcards in visible kind application] ; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $ - unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- Urgh! see Note [Wildcards in visible kind application] - -- ToDo: must kill this ridiculous messing with DynFlags - tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind + tc_lhs_type arg_mode hs_ki_arg exp_kind - ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind) + ; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind) ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg ; go (n+1) fun' subst' inner_ki hs_args } @@ -1241,7 +1398,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- "normal" case | otherwise - -> do { traceTc "tcInferApps (vis normal app)" + -> do { traceTc "tcInferTyApps (vis normal app)" (vcat [ ppr ki_binder , ppr arg , ppr (tyBinderType ki_binder) @@ -1249,7 +1406,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args ; let exp_kind = substTy subst $ tyBinderType ki_binder ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $ tc_lhs_type mode arg exp_kind - ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind) + ; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind) ; (subst', fun') <- mkAppTyM subst fun ki_binder arg' ; go (n+1) fun' subst' inner_ki args } @@ -1263,7 +1420,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- This zonk is essential, to expose the fruits -- of matchExpectedFunKind to the 'go' loop - ; traceTc "tcInferApps (no binder)" $ + ; traceTc "tcInferTyApps (no binder)" $ vcat [ ppr fun <+> dcolon <+> ppr fun_ki , ppr arrows_needed , ppr co @@ -1272,7 +1429,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- Use go_init to establish go's INVARIANT where instantiate ki_binder inner_ki - = do { traceTc "tcInferApps (need to instantiate)" + = do { traceTc "tcInferTyApps (need to instantiate)" (vcat [ ppr ki_binder, ppr subst]) ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder ; go n (mkAppTy fun arg') subst' inner_ki all_args } @@ -1375,7 +1532,7 @@ The way in which tcTypeKind can crash is in applications if 'a' is a type variable whose kind doesn't have enough arrows or foralls. (The crash is in piResultTys.) -The loop in tcInferApps has to be very careful to maintain the (PKTI). +The loop in tcInferTyApps has to be very careful to maintain the (PKTI). For example, suppose kappa is a unification variable We have already unified kappa := Type @@ -1387,7 +1544,7 @@ If we call tcTypeKind on that, we'll crash, because the (un-zonked) kind of 'a' is just kappa, not an arrow kind. So we must zonk first. So the type inference engine is very careful when building applications. -This happens in tcInferApps. Suppose we are kind-checking the type (a Int), +This happens in tcInferTyApps. Suppose we are kind-checking the type (a Int), where (a :: kappa). Then in tcInferApps we'll run out of binders on a's kind, so we'll call matchExpectedFunKind, and unify kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2) @@ -1530,10 +1687,10 @@ tcHsMbContext Nothing = return [] tcHsMbContext (Just cxt) = tcHsContext cxt tcHsContext :: LHsContext GhcRn -> TcM [PredType] -tcHsContext = tc_hs_context typeLevelMode +tcHsContext cxt = tc_hs_context (mkMode TypeLevel) cxt tcLHsPredType :: LHsType GhcRn -> TcM PredType -tcLHsPredType = tc_lhs_pred typeLevelMode +tcLHsPredType pred = tc_lhs_pred (mkMode TypeLevel) pred tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType] tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt) @@ -1553,7 +1710,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference] - unless (isTypeLevel (mode_level mode)) + unless (isTypeLevel (mode_tyki mode)) (promotionErr name TyConPE) ; check_tc tc_tc ; return (mkTyConTy tc_tc, tyConKind tc_tc) } @@ -1584,7 +1741,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon where check_tc :: TyCon -> TcM () check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds - ; unless (isTypeLevel (mode_level mode) || + ; unless (isTypeLevel (mode_tyki mode) || data_kinds || isKindTyCon tc) $ promotionErr name NoDataKindsTC } @@ -1731,8 +1888,6 @@ in the e2 example, we'll desugar the type, zonking the kind unification variables as we go. When we encounter the unconstrained kappa, we want to default it to '*', not to (Any *). -Help functions for type applications -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -} addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a @@ -1744,98 +1899,12 @@ addTypeCtxt (L _ ty) thing where doc = text "In the type" <+> quotes (ppr ty) -{- -************************************************************************ + +{- ********************************************************************* * * Type-variable binders -%* * -%************************************************************************ - -Note [Keeping implicitly quantified variables in order] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When the user implicitly quantifies over variables (say, in a type -signature), we need to come up with some ordering on these variables. -This is done by bumping the TcLevel, bringing the tyvars into scope, -and then type-checking the thing_inside. The constraints are all -wrapped in an implication, which is then solved. Finally, we can -zonk all the binders and then order them with scopedSort. - -It's critical to solve before zonking and ordering in order to uncover -any unifications. You might worry that this eager solving could cause -trouble elsewhere. I don't think it will. Because it will solve only -in an increased TcLevel, it can't unify anything that was mentioned -elsewhere. Additionally, we require that the order of implicitly -quantified variables is manifest by the scope of these variables, so -we're not going to learn more information later that will help order -these variables. - -Note [Recipe for checking a signature] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Checking a user-written signature requires several steps: - - 1. Generate constraints. - 2. Solve constraints. - 3. Promote tyvars and/or kind-generalize. - 4. Zonk. - 5. Check validity. - -There may be some surprises in here: - -Step 2 is necessary for two reasons: most signatures also bring -implicitly quantified variables into scope, and solving is necessary -to get these in the right order (see Note [Keeping implicitly -quantified variables in order]). Additionally, solving is necessary in -order to kind-generalize correctly: otherwise, we do not know which -metavariables are left unsolved. - -Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to -kindGeneralize{All,Some,None}. Here, we have to deal with the fact that -metatyvars generated in the type may have a bumped TcLevel, because explicit -foralls raise the TcLevel. To avoid these variables from ever being visible in -the surrounding context, we must obey the following dictum: - - Every metavariable in a type must either be - (A) generalized, or - (B) promoted, or See Note [Promotion in signatures] - (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType - -The kindGeneralize functions do not require pre-zonking; they zonk as they -go. - -If you are actually doing kind-generalization, you need to bump the level -before generating constraints, as we will only generalize variables with -a TcLevel higher than the ambient one. - -After promoting/generalizing, we need to zonk again because both -promoting and generalizing fill in metavariables. - -Note [Promotion in signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If an unsolved metavariable in a signature is not generalized -(because we're not generalizing the construct -- e.g., pattern -sig -- or because the metavars are constrained -- see kindGeneralizeSome) -we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables] -in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing -and the reinstantiating with a fresh metavariable at the current level. -So in some sense, we generalize *all* variables, but then re-instantiate -some of them. - -Here is an example of why we must promote: - foo (x :: forall a. a -> Proxy b) = ... - -In the pattern signature, `b` is unbound, and will thus be brought into -scope. We do not know its kind: it will be assigned kappa[2]. Note that -kappa is at TcLevel 2, because it is invented under a forall. (A priori, -the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel -than the surrounding context.) This kappa cannot be solved for while checking -the pattern signature (which is not kind-generalized). When we are checking -the *body* of foo, though, we need to unify the type of x with the argument -type of bar. At this point, the ambient TcLevel is 1, and spotting a -matavariable with level 2 would violate the (WantedTvInv) invariant of -Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing, -we promote the metavariable to level 1. This is all done in kindGeneralizeNone. - --} +* * +********************************************************************* -} tcNamedWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) @@ -1844,22 +1913,119 @@ tcNamedWildCardBinders :: [Name] -- plain wildcards _ are anonymous and dealt with by HsWildCardTy -- Soe Note [The wildcard story for types] in GHC.Hs.Type tcNamedWildCardBinders wc_names thing_inside - = do { wcs <- mapM (const newWildTyVar) wc_names + = do { wcs <- mapM newNamedWildTyVar wc_names ; let wc_prs = wc_names `zip` wcs ; tcExtendNameTyVarEnv wc_prs $ thing_inside wc_prs } -newWildTyVar :: TcM TcTyVar +newNamedWildTyVar :: Name -> TcM TcTyVar -- ^ New unification variable '_' for a wildcard -newWildTyVar +newNamedWildTyVar _name -- Currently ignoring the "_x" wildcard name used in the type = do { kind <- newMetaKindVar - ; uniq <- newUnique ; details <- newMetaDetails TauTv - ; let name = mkSysTvName uniq (fsLit "_") - tyvar = mkTcTyVar name kind details + ; wc_name <- newMetaTyVarName (fsLit "w") -- See Note [Wildcard names] + ; let tyvar = mkTcTyVar wc_name kind details ; traceTc "newWildTyVar" (ppr tyvar) ; return tyvar } +--------------------------- +tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType +tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }) + ty exp_kind + -- hole_lvl: see Note [Checking partial type signatures] + -- esp the bullet on nested forall types + = do { kv_details <- newTauTvDetailsAtLevel hole_lvl + ; kv_name <- newMetaTyVarName (fsLit "k") + ; wc_details <- newTauTvDetailsAtLevel hole_lvl + ; wc_name <- newMetaTyVarName (fsLit wc_nm) + ; let kv = mkTcTyVar kv_name liftedTypeKind kv_details + wc_kind = mkTyVarTy kv + wc_tv = mkTcTyVar wc_name wc_kind wc_details + + ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes) + ; when emit_holes $ + emitAnonTypeHole wc_tv + -- Why the 'when' guard? + -- See Note [Wildcards in visible kind application] + + -- You might think that this would always just unify + -- wc_kind with exp_kind, so we could avoid even creating kv + -- But the level numbers might not allow that unification, + -- so we have to do it properly (T14140a) + ; checkExpectedKind ty (mkTyVarTy wc_tv) wc_kind exp_kind } + where + -- See Note [Wildcard names] + wc_nm = case hole_mode of + HM_Sig -> "w" + HM_FamPat -> "_" + HM_VTA -> "w" + + emit_holes = case hole_mode of + HM_Sig -> True + HM_FamPat -> False + HM_VTA -> False + +tcAnonWildCardOcc mode ty _ +-- mode_holes is Nothing. Should not happen, because renamer +-- should already have rejected holes in unexpected places + = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty) + +{- Note [Wildcard names] +~~~~~~~~~~~~~~~~~~~~~~~~ +So we hackily use the mode_holes flag to control the name used +for wildcards: + +* For proper holes (whether in a visible type application (VTA) or no), + we rename the '_' to 'w'. This is so that we see variables like 'w0' + or 'w1' in error messages, a vast improvement upon '_0' and '_1'. For + example, we prefer + Found type wildcard ‘_’ standing for ‘w0’ + over + Found type wildcard ‘_’ standing for ‘_1’ + + Even in the VTA case, where we do not emit an error to be printed, we + want to do the renaming, as the variables may appear in other, + non-wildcard error messages. + +* However, holes in the left-hand sides of type families ("type + patterns") stand for type variables which we do not care to name -- + much like the use of an underscore in an ordinary term-level + pattern. When we spot these, we neither wish to generate an error + message nor to rename the variable. We don't rename the variable so + that we can pretty-print a type family LHS as, e.g., + F _ Int _ = ... + and not + F w1 Int w2 = ... + + See also Note [Wildcards in family instances] in + GHC.Rename.Module. The choice of HM_FamPat is made in + tcFamTyPats. There is also some unsavory magic, relying on that + underscore, in GHC.Core.Coercion.tidyCoAxBndrsForUser. + +Note [Wildcards in visible kind application] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are cases where users might want to pass in a wildcard as a visible kind +argument, for instance: + +data T :: forall k1 k2. k1 → k2 → Type where + MkT :: T a b +x :: T @_ @Nat False n +x = MkT + +So we should allow '@_' without emitting any hole constraints, and +regardless of whether PartialTypeSignatures is enabled or not. But how +would the typechecker know which '_' is being used in VKA and which is +not when it calls emitNamedTypeHole in +tcHsPartialSigType on all HsWildCardBndrs? The solution is to neither +rename nor include unnamed wildcards in HsWildCardBndrs, but instead +give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc. + +And whenever we see a '@', we set mode_holes to HM_VKA, so that +we do not call emitAnonTypeHole in tcAnonWildCardOcc. +See related Note [Wildcards in visible type application] here and +Note [The wildcard story for types] in GHC.Hs.Type +-} + {- ********************************************************************* * * Kind inference for type declarations @@ -2703,8 +2869,17 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv -> TcM a -> TcM ([VarBndr TyVar flag], a) -bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar) -bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar) +bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M + :: (OutputableBndrFlag flag) + => TcTyMode + -> [LHsTyVarBndr flag GhcRn] + -> TcM a + -> TcM ([VarBndr TyVar flag], a) + +bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) newSkolemTyVar) +bindExplicitTKBndrs_Skol_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) newSkolemTyVar) +bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) cloneTyVarTyVar) +bindExplicitTKBndrs_Tv_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) cloneTyVarTyVar) -- newSkolemTyVar: see Note [Non-cloning for tyvar binders] -- cloneTyVarTyVar: see Note [Cloning for tyvar binders] @@ -2752,13 +2927,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside ; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) } ----------------- -tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar) +tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar) -> HsTyVarBndr flag GhcRn -> TcM TcTyVar -tcHsTyVarBndr new_tv (UserTyVar _ _ (L _ tv_nm)) +tcHsTyVarBndr _ new_tv (UserTyVar _ _ (L _ tv_nm)) = do { kind <- newMetaKindVar ; new_tv tv_nm kind } -tcHsTyVarBndr new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) - = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind +tcHsTyVarBndr mode new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) + = do { kind <- tc_lhs_kind_sig mode (TyVarBndrKindCtxt tv_nm) lhs_kind ; new_tv tv_nm kind } ----------------- @@ -2861,15 +3036,14 @@ kindGeneralizeSome should_gen kind_or_type ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen) - ; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote) + ; _ <- promoteTyVarSet to_promote ; qkvs <- quantifyTyVars dvs' ; traceTc "kindGeneralizeSome }" $ vcat [ text "Kind or type:" <+> ppr kind_or_type , text "dvs:" <+> ppr dvs , text "dvs':" <+> ppr dvs' - , text "to_promote:" <+> pprTyVars (dVarSetElems to_promote) - , text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted) + , text "to_promote:" <+> ppr to_promote , text "qkvs:" <+> pprTyVars qkvs ] ; return qkvs } @@ -3046,6 +3220,7 @@ data DataSort checkDataKindSig :: DataSort -> Kind -> TcM () checkDataKindSig data_sort kind = do dflags <- getDynFlags + traceTc "checkDataKindSig" (ppr kind) checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags) where pp_dec :: SDoc @@ -3211,19 +3386,20 @@ tcHsPartialSigType ctxt sig_ty , hsib_body = hs_ty } <- ib_ty , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty = addSigCtxt ctxt hs_ty $ - do { (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau))) + do { mode <- mkHoleMode TypeLevel HM_Sig + ; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau))) <- solveLocalEqualities "tcHsPartialSigType" $ - -- This solveLocalEqualiltes fails fast if there are - -- insoluble equalities. See GHC.Tc.Solver - -- Note [Fail fast if there are insoluble kind equalities] + -- See Note [Failure in local type signatures] tcNamedWildCardBinders sig_wcs $ \ wcs -> - bindImplicitTKBndrs_Tv implicit_hs_tvs $ - bindExplicitTKBndrs_Tv explicit_hs_tvs $ + bindImplicitTKBndrs_Tv implicit_hs_tvs $ + bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $ do { -- Instantiate the type-class context; but if there -- is an extra-constraints wildcard, just discard it here - (theta, wcx) <- tcPartialContext hs_ctxt + (theta, wcx) <- tcPartialContext mode hs_ctxt - ; tau <- tcHsOpenType hs_tau + ; ek <- newOpenTypeKind + ; tau <- addTypeCtxt hs_tau $ + tc_lhs_type mode hs_tau ek ; return (wcs, wcx, theta, tau) } @@ -3241,10 +3417,12 @@ tcHsPartialSigType ctxt sig_ty ; mapM_ emitNamedTypeHole wcs -- Zonk, so that any nested foralls can "see" their occurrences - -- See Note [Checking partial type signatures], in - -- the bullet on Nested foralls. - ; theta <- mapM zonkTcType theta - ; tau <- zonkTcType tau + -- See Note [Checking partial type signatures], and in particular + -- Note [Levels for wildcards] + ; implicit_tvbndrs <- mapM zonkInvisTVBinder implicit_tvbndrs + ; explicit_tvbndrs <- mapM zonkInvisTVBinder explicit_tvbndrs + ; theta <- mapM zonkTcType theta + ; tau <- zonkTcType tau -- We return a proper (Name,InvisTVBinder) environment, to be sure that -- we bring the right name into scope in the function body. @@ -3259,16 +3437,16 @@ tcHsPartialSigType ctxt sig_ty ; traceTc "tcHsPartialSigType" (ppr tv_prs) ; return (wcs, wcx, tv_prs, theta, tau) } -tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType) -tcPartialContext hs_theta +tcPartialContext :: TcTyMode -> HsContext GhcRn -> TcM (TcThetaType, Maybe TcType) +tcPartialContext mode hs_theta | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta - , L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last + , L wc_loc ty@(HsWildCardTy _) <- ignoreParens hs_ctxt_last = do { wc_tv_ty <- setSrcSpan wc_loc $ - tcAnonWildCardOcc wc constraintKind - ; theta <- mapM tcLHsPredType hs_theta1 + tcAnonWildCardOcc mode ty constraintKind + ; theta <- mapM (tc_lhs_pred mode) hs_theta1 ; return (theta, Just wc_tv_ty) } | otherwise - = do { theta <- mapM tcLHsPredType hs_theta + = do { theta <- mapM (tc_lhs_pred mode) hs_theta ; return (theta, Nothing) } {- Note [Checking partial type signatures] @@ -3312,29 +3490,48 @@ we do the following g x = True It's really as if we'd written two distinct signatures. -* Nested foralls. Consider - f :: forall b. (forall a. a -> _) -> b - We do /not/ allow the "_" to be instantiated to 'a'; but we do - (as before) allow it to be instantiated to the (top level) 'b'. - Why not? Because suppose - f x = (x True, x 'c') - We must instantiate that (forall a. a -> _) when typechecking - f's body, so we must know precisely where all the a's are; they - must not be hidden under (filled-in) unification variables! - - We achieve this in the usual way: we push a level at a forall, - so now the unification variable for the "_" can't unify with - 'a'. - -* Just as for ordinary signatures, we must zonk the type after - kind-checking it, to ensure that all the nested forall binders can - see their occurrenceds +* Nested foralls. See Note [Levels for wildcards] + +* Just as for ordinary signatures, we must solve local equalities and + zonk the type after kind-checking it, to ensure that all the nested + forall binders can "see" their occurrenceds Just as for ordinary signatures, this zonk also gets any Refl casts out of the way of instantiation. Example: #18008 had foo :: (forall a. (Show a => blah) |> Refl) -> _ and that Refl cast messed things up. See #18062. +Note [Levels for wildcards] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f :: forall b. (forall a. a -> _) -> b +We do /not/ allow the "_" to be instantiated to 'a'; although we do +(as before) allow it to be instantiated to the (top level) 'b'. +Why not? Suppose + f x = (x True, x 'c') + +During typecking the RHS we must instantiate that (forall a. a -> _), +so we must know /precisely/ where all the a's are; they must not be +hidden under (possibly-not-yet-filled-in) unification variables! + +We achieve this as follows: + +- For /named/ wildcards such sas + g :: forall b. (forall la. a -> _x) -> b + there is no problem: we create them at the outer level (ie the + ambient level of teh signature itself), and push the level when we + go inside a forall. So now the unification variable for the "_x" + can't unify with skolem 'a'. + +- For /anonymous/ wildcards, such as 'f' above, we carry the ambient + level of the signature to the hole in the TcLevel part of the + mode_holes field of TcTyMode. Then, in tcAnonWildCardOcc we us that + level (and /not/ the level ambient at the occurrence of "_") to + create the unification variable for the wildcard. That is the sole + purpose of the TcLevel in the mode_holes field: to transport the + ambient level of the signature down to the anonymous wildcard + occurrences. + Note [Extra-constraint holes in partial type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -3399,14 +3596,16 @@ tcHsPatSigType ctxt , hsps_body = hs_ty }) = addSigCtxt ctxt hs_ty $ do { sig_tkv_prs <- mapM new_implicit_tv sig_ns + ; mode <- mkHoleMode TypeLevel HM_Sig ; (wcs, sig_ty) - <- solveLocalEqualities "tcHsPatSigType" $ - -- Always solve local equalities if possible, - -- else casts get in the way of deep skolemisation - -- (#16033) + <- addTypeCtxt hs_ty $ + solveLocalEqualities "tcHsPatSigType" $ + -- See Note [Failure in local type signatures] + -- and c.f #16033 tcNamedWildCardBinders sig_wcs $ \ wcs -> tcExtendNameTyVarEnv sig_tkv_prs $ - do { sig_ty <- tcHsOpenType hs_ty + do { ek <- newOpenTypeKind + ; sig_ty <- tc_lhs_type mode hs_ty ek ; return (wcs, sig_ty) } ; mapM_ emitNamedTypeHole wcs @@ -3509,10 +3708,15 @@ It does sort checking and desugaring at the same time, in one single pass. tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind tcLHsKindSig ctxt hs_kind + = tc_lhs_kind_sig (mkMode KindLevel) ctxt hs_kind + +tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind +tc_lhs_kind_sig mode ctxt hs_kind -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType -- Result is zonked - = do { kind <- solveLocalEqualities "tcLHsKindSig" $ - tc_lhs_kind kindLevelMode hs_kind + = do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $ + solveLocalEqualities "tcLHsKindSig" $ + tc_lhs_type mode hs_kind liftedTypeKind ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind) -- No generalization: ; kindGeneralizeNone kind @@ -3528,11 +3732,6 @@ tcLHsKindSig ctxt hs_kind ; traceTc "tcLHsKindSig2" (ppr kind) ; return kind } -tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind -tc_lhs_kind mode k - = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $ - tc_lhs_type (kindLevel mode) k liftedTypeKind - promotionErr :: Name -> PromotionErr -> TcM a promotionErr name err = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here") diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index 350be10236..b9eaad4adb 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -36,9 +36,10 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRhoNC, tcInferRho - , tcCheckId, tcLExpr, tcLExprNC, tcExpr - , tcCheckExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC + , tcMonoExpr, tcMonoExprNC, tcExpr + , tcCheckMonoExpr, tcCheckMonoExprNC + , tcCheckPolyExpr, tcCheckId ) import GHC.Types.Basic (LexicalFixity(..)) import GHC.Hs @@ -79,17 +80,11 @@ import Control.Arrow ( second ) @FunMonoBind@. The second argument is the name of the function, which is used in error messages. It checks that all the equations have the same number of arguments before using @tcMatches@ to do the work. - -Note [Polymorphic expected type for tcMatchesFun] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -tcMatchesFun may be given a *sigma* (polymorphic) type -so it must be prepared to use tcSkolemise to skolemise it. -See Note [sig_tau may be polymorphic] in GHC.Tc.Gen.Pat. -} tcMatchesFun :: Located Name -> MatchGroup GhcRn (LHsExpr GhcRn) - -> ExpSigmaType -- Expected type of function + -> ExpRhoType -- Expected type of function -> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId)) -- Returns type of body tcMatchesFun fn@(L _ fun_name) matches exp_ty @@ -102,20 +97,17 @@ tcMatchesFun fn@(L _ fun_name) matches exp_ty traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty) ; checkArgs fun_name matches - ; (wrap_gen, (wrap_fun, group)) - <- tcSkolemiseET (FunSigCtxt fun_name True) exp_ty $ \ exp_rho -> - -- Note [Polymorphic expected type for tcMatchesFun] - do { (matches', wrap_fun) - <- matchExpectedFunTys herald arity exp_rho $ - \ pat_tys rhs_ty -> - tcMatches match_ctxt pat_tys rhs_ty matches - ; return (wrap_fun, matches') } - ; return (wrap_gen <.> wrap_fun, group) } + ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty -> + -- NB: exp_type may be polymorphic, but + -- matchExpectedFunTys can cope with that + tcMatches match_ctxt pat_tys rhs_ty matches } where - arity = matchGroupArity matches + arity = matchGroupArity matches herald = text "The equation(s) for" <+> quotes (ppr fun_name) <+> text "have" - what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness } + ctxt = GenSigCtxt -- Was: FunSigCtxt fun_name True + -- But that's wrong for f :: Int -> forall a. blah + what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness } match_ctxt = MC { mc_what = what, mc_body = tcBody } strictness | [L _ match] <- unLoc $ mg_alts matches @@ -144,10 +136,10 @@ tcMatchesCase ctxt scrut_ty matches res_ty tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify -> TcMatchCtxt HsExpr -> MatchGroup GhcRn (LHsExpr GhcRn) - -> ExpRhoType -- deeply skolemised - -> TcM (MatchGroup GhcTcId (LHsExpr GhcTcId), HsWrapper) + -> ExpRhoType + -> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId)) tcMatchLambda herald match_ctxt match res_ty - = matchExpectedFunTys herald n_pats res_ty $ \ pat_tys rhs_ty -> + = matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty -> tcMatches match_ctxt pat_tys rhs_ty match where n_pats | isEmptyMatchGroup match = 1 -- must be lambda-case @@ -332,7 +324,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt) tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId) tcBody body res_ty = do { traceTc "tcBody" (ppr res_ty) - ; tcLExpr body res_ty + ; tcMonoExpr body res_ty } {- @@ -412,7 +404,7 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside tcGuardStmt :: TcExprStmtChecker tcGuardStmt _ (BodyStmt _ guard _ _) res_ty thing_inside - = do { guard' <- tcLExpr guard (mkCheckExpType boolTy) + = do { guard' <- tcCheckMonoExpr guard boolTy ; thing <- thing_inside res_ty ; return (BodyStmt boolTy guard' noSyntaxExpr noSyntaxExpr, thing) } @@ -445,21 +437,21 @@ tcLcStmt :: TyCon -- The list type constructor ([]) -> TcExprStmtChecker tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside - = do { body' <- tcLExprNC body elt_ty + = do { body' <- tcMonoExprNC body elt_ty ; thing <- thing_inside (panic "tcLcStmt: thing_inside") ; return (LastStmt x body' noret noSyntaxExpr, thing) } -- A generator, pat <- rhs tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside = do { pat_ty <- newFlexiTyVarTy liftedTypeKind - ; rhs' <- tcLExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty]) + ; rhs' <- tcCheckMonoExpr rhs (mkTyConApp m_tc [pat_ty]) ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside elt_ty ; return (mkTcBindStmt pat' rhs', thing) } -- A boolean guard tcLcStmt _ _ (BodyStmt _ rhs _ _) elt_ty thing_inside - = do { rhs' <- tcLExpr rhs (mkCheckExpType boolTy) + = do { rhs' <- tcCheckMonoExpr rhs boolTy ; thing <- thing_inside elt_ty ; return (BodyStmt boolTy rhs' noSyntaxExpr noSyntaxExpr, thing) } @@ -517,7 +509,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts by_arrow $ poly_arg_ty `mkVisFunTy` poly_res_ty - ; using' <- tcCheckExpr using using_poly_ty + ; using' <- tcCheckPolyExpr using using_poly_ty ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using' -- 'stmts' returns a result of type (m1_ty tuple_ty), @@ -559,7 +551,7 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside = do { (body', return_op') <- tcSyntaxOp MCompOrigin return_op [SynRho] res_ty $ \ [a_ty] -> - tcLExprNC body (mkCheckExpType a_ty) + tcCheckMonoExprNC body a_ty ; thing <- thing_inside (panic "tcMcStmt: thing_inside") ; return (LastStmt x body' noret return_op', thing) } @@ -575,7 +567,7 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', pat', thing, new_res_ty) } @@ -607,7 +599,7 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside <- tcSyntaxOp MCompOrigin guard_op [SynAny] (mkCheckExpType rhs_ty) $ \ [test_ty] -> - tcLExpr rhs (mkCheckExpType test_ty) + tcCheckMonoExpr rhs test_ty ; thing <- thing_inside (mkCheckExpType new_res_ty) ; return (thing, rhs', rhs_ty, guard_op') } ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } @@ -667,8 +659,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap (mkCheckExpType using_arg_ty) $ \res_ty' -> do { by' <- case by of Nothing -> return Nothing - Just e -> do { e' <- tcLExpr e - (mkCheckExpType by_e_ty) + Just e -> do { e' <- tcCheckMonoExpr e by_e_ty ; return (Just e') } -- Find the Ids (and hence types) of all old binders @@ -693,7 +684,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap --------------- Typecheck the 'fmap' function ------------- ; fmap_op' <- case form of ThenForm -> return noExpr - _ -> fmap unLoc . tcCheckExpr (noLoc fmap_op) $ + _ -> fmap unLoc . tcCheckPolyExpr (noLoc fmap_op) $ mkInfForAllTy alphaTyVar $ mkInfForAllTy betaTyVar $ (alphaTy `mkVisFunTy` betaTy) @@ -703,7 +694,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap --------------- Typecheck the 'using' function ------------- -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c)) - ; using' <- tcCheckExpr using using_poly_ty + ; using' <- tcCheckPolyExpr using using_poly_ty ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using' --------------- Building the bindersMap ---------------- @@ -765,7 +756,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside (m_ty `mkAppTy` betaTy) `mkVisFunTy` (m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy]) - ; mzip_op' <- unLoc `fmap` tcCheckExpr (noLoc mzip_op) mzip_ty + ; mzip_op' <- unLoc `fmap` tcCheckPolyExpr (noLoc mzip_op) mzip_ty -- type dummies since we don't know all binder types yet ; id_tys_s <- (mapM . mapM) (const (newFlexiTyVarTy liftedTypeKind)) @@ -827,7 +818,7 @@ tcMcStmt _ stmt _ _ tcDoStmt :: TcExprStmtChecker tcDoStmt _ (LastStmt x body noret _) res_ty thing_inside - = do { body' <- tcLExprNC body res_ty + = do { body' <- tcMonoExprNC body res_ty ; thing <- thing_inside (panic "tcDoStmt: thing_inside") ; return (LastStmt x body' noret noSyntaxExpr, thing) } @@ -840,7 +831,7 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside ((rhs', pat', new_res_ty, thing), bind_op') <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', pat', new_res_ty, thing) } @@ -873,7 +864,7 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside ; ((rhs', rhs_ty, thing), then_op') <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; thing <- thing_inside (mkCheckExpType new_res_ty) ; return (rhs', rhs_ty, thing) } ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } @@ -1043,7 +1034,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside }, pat_ty, exp_ty) = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $ addErrCtxt (pprStmtInCtxt ctxt (mkRnBindStmt pat rhs)) $ - do { rhs' <- tcLExprNC rhs (mkCheckExpType exp_ty) + do { rhs' <- tcCheckMonoExprNC rhs exp_ty ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ return () ; fail_op' <- fmap join . forM fail_op $ \fail -> diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 58f64f84ae..4e30d4bc33 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -30,7 +30,7 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho ) import GHC.Hs import GHC.Tc.Utils.Zonk @@ -397,43 +397,51 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of res) } ViewPat _ expr pat -> do - { - -- We use tcInferRho here. - -- If we have a view function with types like: - -- blah -> forall b. burble - -- then simple-subsumption means that 'forall b' won't be instantiated - -- so we can typecheck the inner pattern with that type - -- An exotic example: - -- pair :: forall a. a -> forall b. b -> (a,b) - -- f (pair True -> x) = ...here (x :: forall b. b -> (Bool,b)) - -- - -- TEMPORARY: pending simple subsumption, use tcInferSigma - -- When removing this, remove it from Expr.hs-boot too - ; (expr',expr_ty) <- tcInferSigma expr + { (expr',expr_ty) <- tcInferRho expr + -- Note [View patterns and polymorphism] -- Expression must be a function ; let expr_orig = lexprCtOrigin expr herald = text "A view pattern expression expects" - ; (expr_wrap1, [inf_arg_ty], inf_res_ty) - <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr_ty - -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty) + ; (expr_wrap1, inf_arg_ty, inf_res_sigma) + <- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty + -- See Note [View patterns and polymorphism] + -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma) -- Check that overall pattern is more polymorphic than arg type ; expr_wrap2 <- tc_sub_type penv pat_ty inf_arg_ty -- expr_wrap2 :: pat_ty "->" inf_arg_ty - -- Pattern must have inf_res_ty - ; (pat', res) <- tc_lpat (mkCheckExpType inf_res_ty) penv pat thing_inside + -- Pattern must have inf_res_sigma + ; (pat', res) <- tc_lpat (mkCheckExpType inf_res_sigma) penv pat thing_inside ; pat_ty <- readExpType pat_ty ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper - pat_ty inf_res_ty doc - -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->" - -- (pat_ty -> inf_res_ty) + pat_ty inf_res_sigma doc + -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" + -- (pat_ty -> inf_res_sigma) expr_wrap = expr_wrap2' <.> expr_wrap1 doc = text "When checking the view pattern function:" <+> (ppr expr) ; return (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res)} +{- Note [View patterns and polymorphism] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this exotic example: + pair :: forall a. Bool -> a -> forall b. b -> (a,b) + + f :: Int -> blah + f (pair True -> x) = ...here (x :: forall b. b -> (Int,b)) + +The expresion (pair True) should have type + pair True :: Int -> forall b. b -> (Int,b) +so that it is ready to consume the incoming Int. It should be an +arrow type (t1 -> t2); hence using (tcInferRho expr). + +Then, when taking that arrow apart we want to get a *sigma* type +(forall b. b->(Int,b)), because that's what we want to bind 'x' to. +Fortunately that's what matchExpectedFunTySigma returns anyway. +-} + -- Type signatures in patterns -- See Note [Pattern coercions] below SigPat _ pat sig_ty -> do diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index c788f15437..63377c74d5 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -199,7 +199,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs do { -- See Note [Solve order for RULES] ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs) ; (rhs', rhs_wanted) <- captureConstraints $ - tcLExpr rhs (mkCheckExpType rule_ty) + tcCheckMonoExpr rhs rule_ty ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } } diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index fb313d9297..2ac2823fb5 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -635,6 +635,7 @@ to connect the two, something like This wrapper is put in the TcSpecPrag, in the ABExport record of the AbsBinds. + f :: (Eq a, Ix b) => a -> b -> Bool {-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-} f = <poly_rhs> @@ -674,12 +675,13 @@ delicate, but works. Some wrinkles -1. We don't use full-on tcSubType, because that does co and contra - variance and that in turn will generate too complex a LHS for the - RULE. So we use a single invocation of skolemise / - topInstantiate in tcSpecWrapper. (Actually I think that even - the "deeply" stuff may be too much, because it introduces lambdas, - though I think it can be made to work without too much trouble.) +1. In tcSpecWrapper, rather than calling tcSubType, we directly call + skolemise/instantiate. That is mainly because of wrinkle (2). + + Historical note: in the past, tcSubType did co/contra stuff, which + could generate too complex a LHS for the RULE, which was another + reason for not using tcSubType. But that reason has gone away + with simple subsumption (#17775). 2. We need to take care with type families (#5821). Consider type instance F Int = Bool @@ -775,7 +777,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper -- See Note [Handling SPECIALISE pragmas], wrinkle 1 tcSpecWrapper ctxt poly_ty spec_ty = do { (sk_wrap, inst_wrap) - <- tcSkolemise ctxt spec_ty $ \ _ spec_tau -> + <- tcSkolemise ctxt spec_ty $ \ spec_tau -> do { (inst_wrap, tau) <- topInstantiate orig poly_ty ; _ <- unifyType Nothing spec_tau tau -- Deliberately ignore the evidence diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index 8a7b1b0c7f..f1233c55ed 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -288,7 +288,7 @@ tcPendingSplice m_var (PendingRnSplice flavour splice_name expr) = do { meta_ty <- tcMetaTy meta_ty_name -- Expected type of splice, e.g. m Exp ; let expected_type = mkAppTy m_var meta_ty - ; expr' <- tcCheckExpr expr expected_type + ; expr' <- tcCheckPolyExpr expr expected_type ; return (PendingTcSplice splice_name expr') } where meta_ty_name = case flavour of @@ -618,7 +618,7 @@ tcNestedSplice pop_stage (TcPending ps_var lie_var q@(QuoteWrapper _ m_var)) spl ; meta_exp_ty <- tcTExpTy m_var res_ty ; expr' <- setStage pop_stage $ setConstraintVar lie_var $ - tcLExpr expr (mkCheckExpType meta_exp_ty) + tcCheckMonoExpr expr meta_exp_ty ; untypeq <- tcLookupId unTypeQName ; let expr'' = mkHsApp (mkLHsWrap (applyQuoteWrapper q) @@ -647,7 +647,7 @@ tcTopSplice expr res_ty -- Top level splices must still be of type Q (TExp a) ; meta_exp_ty <- tcTExpTy q_type res_ty ; q_expr <- tcTopSpliceExpr Typed $ - tcLExpr expr (mkCheckExpType meta_exp_ty) + tcCheckMonoExpr expr meta_exp_ty ; lcl_env <- getLclEnv ; let delayed_splice = DelayedSplice lcl_env expr res_ty q_expr @@ -684,7 +684,7 @@ runTopSplice (DelayedSplice lcl_env orig_expr res_ty q_expr) captureConstraints $ addErrCtxt (spliceResultDoc zonked_q_expr) $ do { (exp3, _fvs) <- rnLExpr expr2 - ; tcLExpr exp3 (mkCheckExpType zonked_ty)} + ; tcCheckMonoExpr exp3 zonked_ty } ; ev <- simplifyTop wcs ; return $ unLoc (mkHsDictLet (EvBinds ev) res) } @@ -717,7 +717,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc) -- Note that set the level to Splice, regardless of the original level, -- before typechecking the expression. For example: -- f x = $( ...$(g 3) ... ) --- The recursive call to tcCheckExpr will simply expand the +-- The recursive call to tcCheckPolyExpr will simply expand the -- inner escape before dealing with the outer one tcTopSpliceExpr isTypedSplice tc_action @@ -1438,7 +1438,7 @@ reifyInstances th_nm th_tys <- pushTcLevelM_ $ solveEqualities $ -- Avoid error cascade if there are unsolved bindImplicitTKBndrs_Skol tv_names $ - fst <$> tcLHsType rn_ty + tcInferLHsType rn_ty ; ty <- zonkTcTypeToType ty -- Substitute out the meta type variables -- In particular, the type might have kind diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 267a36cd89..300a870709 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -1781,11 +1781,11 @@ check_main dflags tcg_env explicit_mod_hdr export_ies ; res_ty <- newFlexiTyVarTy liftedTypeKind ; let io_ty = mkTyConApp ioTyCon [res_ty] skol_info = SigSkol (FunSigCtxt main_name False) io_ty [] + main_expr_rn = L loc (HsVar noExtField (L loc main_name)) ; (ev_binds, main_expr) <- checkConstraints skol_info [] [] $ addErrCtxt mainCtxt $ - tcLExpr (L loc (HsVar noExtField (L loc main_name))) - (mkCheckExpType io_ty) + tcCheckMonoExpr main_expr_rn io_ty -- See Note [Root-main Id] -- Construct the binding @@ -2476,6 +2476,7 @@ data TcRnExprMode = TM_Inst -- ^ Instantiate the type fully (:type) | TM_Default -- ^ Default the type eagerly (:type +d) -- | tcRnExpr just finds the type of an expression +-- for :type tcRnExpr :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs @@ -2590,7 +2591,7 @@ tcRnType hsc_env flexi normalise rdr_type solveEqualities $ tcNamedWildCardBinders wcs $ \ wcs' -> do { mapM_ emitNamedTypeHole wcs' - ; tcLHsTypeUnsaturated rn_type } + ; tcInferLHsTypeUnsaturated rn_type } -- Do kind generalisation; see Note [Kind-generalise in tcRnType] ; kvs <- kindGeneralizeAll kind @@ -2623,7 +2624,7 @@ considers this example, with -fprint-explicit-foralls enabled: 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 deeply instantiate the type and then regeneralize, as discussed + This means we instantiate the type and then regeneralize, as discussed in #11376. > :type foo @Int diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index b1017de024..8736206188 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -16,8 +16,7 @@ module GHC.Tc.Solver( simpl_top, - promoteTyVar, - promoteTyVarSet, + promoteTyVarSet, emitFlatConstraints, -- For Rules we need these solveWanteds, solveWantedsAndDrop, @@ -65,7 +64,6 @@ import Control.Monad import Data.Foldable ( toList ) import Data.List ( partition ) import Data.List.NonEmpty ( NonEmpty(..) ) -import GHC.Data.Maybe ( isJust ) {- ********************************************************************************* @@ -162,27 +160,143 @@ simplifyTop wanteds -- should generally bump the TcLevel to make sure that this run of the solver -- doesn't affect anything lying around. solveLocalEqualities :: String -> TcM a -> TcM a +-- Note [Failure in local type signatures] solveLocalEqualities callsite thing_inside = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside - ; emitConstraints wanted + ; emitFlatConstraints wanted + ; return res } - -- See Note [Fail fast if there are insoluble kind equalities] - ; when (insolubleWC wanted) $ - failM +emitFlatConstraints :: WantedConstraints -> TcM () +-- See Note [Failure in local type signatures] +emitFlatConstraints wanted + = do { wanted <- TcM.zonkWC wanted + ; case floatKindEqualities wanted of + Nothing -> do { traceTc "emitFlatConstraints: failing" (ppr wanted) + ; emitConstraints wanted -- So they get reported! + ; failM } + Just (simples, holes) + -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples) + ; traceTc "emitFlatConstraints:" $ + vcat [ text "simples:" <+> ppr simples + , text "holes: " <+> ppr holes ] + ; emitHoles holes -- Holes don't need promotion + ; emitSimples simples } } + +floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole) +-- Float out all the constraints from the WantedConstraints, +-- Return Nothing if any constraints can't be floated (captured +-- by skolems), or if there is an insoluble constraint, or +-- IC_Telescope telescope error +floatKindEqualities wc = float_wc emptyVarSet wc + where + float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole) + float_wc trapping_tvs (WC { wc_simple = simples + , wc_impl = implics + , wc_holes = holes }) + | all is_floatable simples + = do { (inner_simples, inner_holes) + <- flatMapBagPairM (float_implic trapping_tvs) implics + ; return ( simples `unionBags` inner_simples + , holes `unionBags` inner_holes) } + | otherwise + = Nothing + where + is_floatable ct + | insolubleEqCt ct = False + | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs + + float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag Hole) + float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_no_eqs = no_eqs + , ic_skols = skols, ic_status = status }) + | isInsolubleStatus status + = Nothing -- A short cut /plus/ we must keep track of IC_BadTelescope + | otherwise + = do { (simples, holes) <- float_wc new_trapping_tvs wanted + ; when (not (isEmptyBag simples) && not no_eqs) $ + Nothing + -- If there are some constraints to float out, but we can't + -- because we don't float out past local equalities + -- (c.f GHC.Tc.Solver.approximateWC), then fail + ; return (simples, holes) } + where + new_trapping_tvs = trapping_tvs `extendVarSetList` skols - ; return res } -{- Note [Fail fast if there are insoluble kind equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Rather like in simplifyInfer, fail fast if there is an insoluble -constraint. Otherwise we'll just succeed in kind-checking a nonsense -type, with a cascade of follow-up errors. +{- Note [Failure in local type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When kind checking a type signature, we like to fail fast if we can't +solve all the kind equality constraints: see Note [Fail fast on kind +errors]. But what about /local/ type signatures, mentioning in-scope +type variables for which there might be given equalities. Here's +an example (T15076b): + + class (a ~ b) => C a b + data SameKind :: k -> k -> Type where { SK :: SameKind a b } + + bar :: forall (a :: Type) (b :: Type). + C a b => Proxy a -> Proxy b -> () + bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y) + +Consider the type singature on 'undefined'. It's ill-kinded unless +a~b. But the superclass of (C a b) means that indeed (a~b). So all +should be well. BUT it's hard to see that when kind-checking the signature +for undefined. We want to emit a residual (a~b) constraint, to solve +later. + +Another possiblity is that we might have something like + F alpha ~ [Int] +where alpha is bound further out, which might become soluble +"later" when we learn more about alpha. So we want to emit +those residual constraints. + +BUT it's no good simply wrapping all unsolved constraints from +a type signature in an implication constraint to solve later. The +problem is that we are going to /use/ that signature, including +instantiate it. Say we have + f :: forall a. (forall b. blah) -> blah2 + f x = <body> +To typecheck the definition of f, we have to instantiate those +foralls. Moreover, any unsolved kind equalities will be coercion +holes in the type. If we naively wrap them in an implication like + forall a. (co1:k1~k2, forall b. co2:k3~k4) +hoping to solve it later, we might end up filling in the holes +co1 and co2 with coercions involving 'a' and 'b' -- but by now +we've instantiated the type. Chaos! + +Moreover, the unsolved constraints might be skolem-escpae things, and +if we proceed with f bound to a nonsensical type, we get a cascade of +follow-up errors. For example polykinds/T12593, T15577, and many others. + +So here's the plan: -For example polykinds/T12593, T15577, and many others. +* solveLocalEqualitiesX: try to solve the constraints (solveLocalEqualitiesX) -Take care to ensure that you emit the insoluble constraints before -failing, because they are what will ultimately lead to the error -messsage! +* buildTvImplication: build an implication for the residual, unsolved + constraint + +* emitFlatConstraints: try to float out every unsolved equalities + inside that implication, in the hope that it constrains only global + type variables, not the locally-quantified ones. + + * If we fail, or find an insoluble constraint, emit the implication, + so that the errors will be reported, and fail. + + * If we succeed in floating all the equalities, promote them and + re-emit them as flat constraint, not wrapped at all (since they + don't mention any of the quantified variables. + +* Note that this float-and-promote step means that anonymous + wildcards get floated to top level, as we want; see + Note [Checking partial type signatures] in GHC.Tc.Gen.HsType. + +All this is done: + +* in solveLocalEqualities, where there is no kind-generalisation + to complicate matters. + +* in GHC.Tc.Gen.HsType.tcHsSigType, where quantification intervenes. + +See also #18062, #11506 -} solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a) @@ -867,7 +981,6 @@ mkResidualConstraints rhs_tclvl ev_binds_var return $ unitBag $ implic1 { ic_tclvl = rhs_tclvl , ic_skols = qtvs - , ic_telescope = Nothing , ic_given = full_theta_vars , ic_wanted = inner_wanted , ic_binds = ev_binds_var @@ -1168,7 +1281,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates = do { -- Promote any tyvars that we cannot generalise -- See Note [Promote momomorphic tyvars] ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) - ; (prom, _) <- promoteTyVarSet mono_tvs + ; any_promoted <- promoteTyVarSet mono_tvs -- Default any kind/levity vars ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} @@ -1186,7 +1299,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates ; case () of _ | some_default -> simplify_cand candidates - | prom -> mapM TcM.zonkTcType candidates + | any_promoted -> mapM TcM.zonkTcType candidates | otherwise -> return candidates } where @@ -1789,9 +1902,9 @@ setImplicationStatus implic@(Implic { ic_status = status checkBadTelescope :: Implication -> TcS Bool -- True <=> the skolems form a bad telescope -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint -checkBadTelescope (Implic { ic_telescope = m_telescope - , ic_skols = skols }) - | isJust m_telescope +checkBadTelescope (Implic { ic_info = info + , ic_skols = skols }) + | ForAllSkol {} <- info = do{ skols <- mapM TcS.zonkTyCoVarKind skols ; return (go emptyVarSet (reverse skols))} @@ -2063,7 +2176,7 @@ we'll get more Givens (a unification is like adding a Given) to allow the implication to make progress. -} -promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar) +promoteTyVar :: TcTyVar -> TcM Bool -- When we float a constraint out of an implication we must restore -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType -- Return True <=> we did some promotion @@ -2075,16 +2188,16 @@ promoteTyVar tv then do { cloned_tv <- TcM.cloneMetaTyVar tv ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) - ; return (True, rhs_tv) } - else return (False, tv) } + ; return True } + else return False } -- Returns whether or not *any* tyvar is defaulted -promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet) +promoteTyVarSet :: TcTyVarSet -> TcM Bool promoteTyVarSet tvs - = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs) - -- non-determinism is OK because order of promotion doesn't matter + = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs) + -- Non-determinism is OK because order of promotion doesn't matter - ; return (or bools, mkVarSet tyvars) } + ; return (or bools) } promoteTyVarTcS :: TcTyVar -> TcS () -- When we float a constraint out of an implication we must restore @@ -2122,7 +2235,7 @@ approximateWC float_past_equalities wc float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) = filterBag (is_floatable trapping_tvs) simples `unionBags` - do_bag (float_implic trapping_tvs) implics + concatMapBag (float_implic trapping_tvs) implics where float_implic :: TcTyCoVarSet -> Implication -> Cts @@ -2134,9 +2247,6 @@ approximateWC float_past_equalities wc where new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp - do_bag :: (a -> Bag c) -> Bag a -> Bag c - do_bag f = foldr (unionBags.f) emptyBag - is_floatable skol_tvs ct | isGivenCt ct = False | insolubleEqCt ct = False @@ -2419,21 +2529,20 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs | otherwise = acc -- Identify which equalities are candidates for floating - -- Float out alpha ~ ty, or ty ~ alpha which might be unified outside + -- Float out alpha ~ ty which might be unified outside -- See Note [Which equalities to float] is_float_eq_candidate ct | pred <- ctPred ct , EqPred NomEq ty1 ty2 <- classifyPredType pred - = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of - (Just tv1, _) -> float_tv_eq_candidate tv1 ty2 - (_, Just tv2) -> float_tv_eq_candidate tv2 ty1 - _ -> False - | otherwise = False - - float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float] - = isMetaTyVar tv1 - && (not (isTyVarTyVar tv1) || isTyVarTy ty2) + = float_eq ty1 ty2 || float_eq ty2 ty1 + | otherwise + = False + float_eq ty1 ty2 + = case getTyVar_maybe ty1 of + Just tv1 -> isMetaTyVar tv1 + && (not (isTyVarTyVar tv1) || isTyVarTy ty2) + Nothing -> False {- Note [Float equalities from under a skolem binding] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2470,6 +2579,12 @@ happen. In particular, float out equalities that are: case, floating out won't help either, and it may affect grouping of error messages. + NB: generally we won't see (ty ~ alpha), with alpha on the right because + of Note [Unification variables on the left] in GHC.Tc.Utils.Unify. + But if we start with (F tys ~ alpha), it will orient as (fmv ~ alpha), + and unflatten back to (F tys ~ alpha). So we must look for alpha on + the right too. Example T4494. + * Nominal. No point in floating (alpha ~R# ty), because we do not unify representational equalities even if alpha is touchable. See Note [Do not unify representational equalities] in GHC.Tc.Solver.Interact. diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 4e828c919c..2fc8664450 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -904,22 +904,23 @@ It is conceivable to do a better job at tracking whether or not a type is flattened, but this is left as future work. (Mar '15) -Note [FunTy and decomposing tycon applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked. -This means that we may very well have a FunTy containing a type of some unknown -kind. For instance, we may have, +Note [Decomposing FunTy] +~~~~~~~~~~~~~~~~~~~~~~~~ +can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This +means that we may very well have a FunTy containing a type of some +unknown kind. For instance, we may have, FunTy (a :: k) Int -Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event -that it sees such a type as it cannot determine the RuntimeReps which the (->) -is applied to. Consequently, it is vital that we instead use -tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case. - -When this happens can_eq_nc' will fail to decompose, zonk, and try again. +Where k is a unification variable. So the calls to getRuntimeRep_maybe may +fail (returning Nothing). In that case we'll fall through, zonk, and try again. Zonking should fill the variable k, meaning that decomposition will succeed the second time around. + +Also note that we require the AnonArgFlag to match. This will stop +us decomposing + (Int -> Bool) ~ (Show a => blah) +It's as if we treat (->) and (=>) as different type constructors. -} canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct) @@ -1003,13 +1004,26 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } --- Try to decompose type constructor applications --- Including FunTy (s -> t) -can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _ - --- See Note [FunTy and decomposing type constructor applications]. - | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1 - , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2 - , not (isTypeFamilyTyCon tc1) +-- Decompose FunTy: (s -> t) and (c => t) +-- NB: don't decompose (Int -> blah) ~ (Show a => blah) +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ + (FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ + | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah) + , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe: + , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy] + , Just ty2a_rep <- getRuntimeRep_maybe ty2a + , Just ty2b_rep <- getRuntimeRep_maybe ty2b + = canDecomposableTyConAppOK ev eq_rel funTyCon + [ty1a_rep, ty1b_rep, ty1a, ty1b] + [ty2a_rep, ty2b_rep, ty2a, ty2b] + +-- Decompose type constructor applications +-- NB: e have expanded type synonyms already +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (TyConApp tc1 tys1) _ + (TyConApp tc2 tys2) _ + | not (isTypeFamilyTyCon tc1) , not (isTypeFamilyTyCon tc2) = canTyConApp ev eq_rel tc1 tys1 tc2 tys2 @@ -1452,15 +1466,13 @@ canTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApps] +-- Neither tc1 nor tc2 is a saturated funTyCon canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getTcSInerts ; if can_decompose inerts - then do { traceTcS "canTyConApp" - (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2) - ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 - ; stopWith ev "Decomposed TyConApp" } + then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 else canEqFailure ev eq_rel ty1 ty2 } -- See Note [Skolem abstract data] (at tyConSkolem) @@ -1476,6 +1488,10 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | otherwise = canEqHardFailure ev ty1 ty2 where + -- Reconstruct the types for error messages. This would do + -- the wrong thing (from a pretty printing point of view) + -- for functions, because we've lost the AnonArgFlag; but + -- in fact we never call canTyConApp on a saturated FunTyCon ty1 = mkTyConApp tc1 tys1 ty2 = mkTyConApp tc2 tys2 @@ -1673,30 +1689,35 @@ Conclusion: canDecomposableTyConAppOK :: CtEvidence -> EqRel -> TyCon -> [TcType] -> [TcType] - -> TcS () + -> TcS (StopOrContinue Ct) -- Precondition: tys1 and tys2 are the same length, hence "OK" canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 = ASSERT( tys1 `equalLength` tys2 ) - case ev of - CtDerived {} - -> unifyDeriveds loc tc_roles tys1 tys2 - - CtWanted { ctev_dest = dest } - -- new_locs and tc_roles are both infinite, so - -- we are guaranteed that cos has the same length - -- as tys1 and tys2 - -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 - ; setWantedEq dest (mkTyConAppCo role tc cos) } - - CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole r ty1 ty2 - , evCoercion $ mkNthCo r i ev_co ) - | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] - , r /= Phantom - , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] - ; emitWorkNC given_evs } + do { traceTcS "canDecomposableTyConAppOK" + (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) + ; case ev of + CtDerived {} + -> unifyDeriveds loc tc_roles tys1 tys2 + + CtWanted { ctev_dest = dest } + -- new_locs and tc_roles are both infinite, so + -- we are guaranteed that cos has the same length + -- as tys1 and tys2 + -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 + ; setWantedEq dest (mkTyConAppCo role tc cos) } + + CtGiven { ctev_evar = evar } + -> do { let ev_co = mkCoVarCo evar + ; given_evs <- newGivenEvVars loc $ + [ ( mkPrimEqPredRole r ty1 ty2 + , evCoercion $ mkNthCo r i ev_co ) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom + , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] + ; emitWorkNC given_evs } + + ; stopWith ev "Decomposed TyConApp" } + where loc = ctEvLoc ev role = eqRelRole eq_rel @@ -1747,7 +1768,8 @@ canEqHardFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 - = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 + = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) + ; (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 ; continueWith (mkIrredCt InsolubleCIS new_ev) } @@ -2007,7 +2029,7 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _ -- this guarantees (TyEq:TV) | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2 - , swapOverTyVars tv1 tv2 + , swapOverTyVars (isGiven ev) tv1 tv2 = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) ; let role = eqRelRole eq_rel sym_co2 = mkTcSymCo co2 diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index ecfa9afa3a..6916357691 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -1175,7 +1175,7 @@ flatten_one (TyConApp tc tys) -- _ -> fmode = flatten_ty_con_app tc tys -flatten_one ty@(FunTy _ ty1 ty2) +flatten_one ty@(FunTy { ft_arg = ty1, ft_res = ty2 }) = do { (xi1,co1) <- flatten_one ty1 ; (xi2,co2) <- flatten_one ty2 ; role <- getRole diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 144021caea..98550132c5 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -2313,18 +2313,18 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 2. Where these kinds come from: Return kinds are processed through several different code paths: - data/newtypes: The return kind is part of the TyCon kind, gotten either + Data/newtypes: The return kind is part of the TyCon kind, gotten either by checkInitialKind (standalone kind signature / CUSK) or inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is then passed to tcDataDefn. - families: The return kind is either written in a standalone signature + Families: The return kind is either written in a standalone signature or extracted from a family declaration in getInitialKind. If a family declaration is missing a result kind, it is assumed to be Type. This assumption is in getInitialKind for CUSKs or get_fam_decl_initial_kind for non-signature & non-CUSK cases. - instances: The data family already has a known kind. The return kind + Instances: The data family already has a known kind. The return kind of an instance is then calculated by applying the data family tycon to the patterns provided, as computed by the typeKind lhs_ty in the end of tcDataFamInstHeader. In the case of an instance written in GADT @@ -2350,10 +2350,9 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 4. Datatype return kind restriction: A data/data-instance return kind must end in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By "end in", we mean we strip any foralls and function arguments off before - checking: this remaining part of the type is returned from - etaExpandAlgTyCon. Note that we do *not* do type family reduction here. - Examples: + checking: this remaining part of the type is returned from etaExpandAlgTyCon. + Examples: data T1 :: Type -- good data T2 :: Bool -> Type -- good data T3 :: Bool -> forall k. Type -- strange, but still accepted @@ -2361,27 +2360,38 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 data T5 :: Bool -- bad data T6 :: Type -> Bool -- bad + Exactly the same applies to data instance (but not data family) + declarations. Examples + data instance D1 :: Type -- good + data instance D2 :: Boool -> Type -- good + + We can "look through" type synonyms + type Star = Type + data T7 :: Bool -> Star -- good (synonym expansion ok) type Arrow = (->) - data T7 :: Arrow Bool Type -- good + data T8 :: Arrow Bool Type -- good (ditto) + But we specifically do *not* do type family reduction here. type family ARROW where ARROW = (->) - data T8 :: ARROW Bool Type -- bad - - type Star = Type - data T9 :: Bool -> Star -- good + data T9 :: ARROW Bool Type -- bad type family F a where F Int = Bool F Bool = Type data T10 :: Bool -> F Bool -- bad + The /principle/ here is that in the TyCon for a data type or data instance, + we must be able to lay out all the type-variable binders, one by one, until + we reach (TYPE xx). There is no place for a cast here. We could add one, + but let's not! + This check is done in checkDataKindSig. For data declarations, this call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl. - However, because data instances in GADT syntax can have two return kinds (see - point (2) above), we must check both return kinds. The user-written return - kind is checked in tc_kind_sig within tcDataFamInstHeader. Examples: +4a Because data instances in GADT syntax can have two return kinds (see + point (2) above), we must check both return kinds. The user-written return + kind is checked by the call to checkDataKindSig in tcDataFamInstDecl. Examples: data family D (a :: Nat) :: k -- good (see Point 6) @@ -2906,36 +2916,11 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; return (qtvs, pats, rhs_ty) } ----------------- -tcFamTyPats :: TyCon - -> HsTyPats GhcRn -- Patterns - -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind) --- Used for both type and data families -tcFamTyPats fam_tc hs_pats - = do { traceTc "tcFamTyPats {" $ - vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ] - - ; let fun_ty = mkTyConApp fam_tc [] - - ; (fam_app, res_kind) <- unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- See Note [Wildcards in family instances] in - -- GHC.Rename.Module - tcInferApps typeLevelMode lhs_fun fun_ty hs_pats - - ; traceTc "End tcFamTyPats }" $ - vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] - - ; return (fam_app, res_kind) } - where - fam_name = tyConName fam_tc - fam_arity = tyConArity fam_tc - lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) - unravelFamInstPats :: TcType -> [TcType] -- Decompose fam_app to get the argument patterns -- -- We expect fam_app to look like (F t1 .. tn) --- tcInferApps is capable of returning ((F ty1 |> co) ty2), +-- tcFamTyPats is capable of returning ((F ty1 |> co) ty2), -- but that can't happen here because we already checked the -- arity of F matches the number of pattern unravelFamInstPats fam_app @@ -4749,20 +4734,20 @@ badDataConTyCon data_con res_ty_tmpl $+$ hang (text "Suggestion: instead use this type signature:") 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty) - -- To construct a type that GHC would accept (suggested_ty), we: - -- - -- 1) Find the existentially quantified type variables and the class - -- predicates from the datacon. (NB: We don't need the universally - -- quantified type variables, since rejigConRes won't substitute them in - -- the result type if it fails, as in this scenario.) - -- 2) Split apart the return type (which is headed by a forall or a - -- context) using tcSplitNestedSigmaTys, collecting the type variables - -- and class predicates we find, as well as the rho type lurking - -- underneath the nested foralls and contexts. - -- 3) Smash together the type variables and class predicates from 1) and - -- 2), and prepend them to the rho type from 2). - (tvs, theta, rho) = tcSplitNestedSigmaTys (dataConUserType data_con) + -- To construct a type that GHC would accept (suggested_ty), we + -- simply drag all the foralls and (=>) contexts to the front + -- of the type. suggested_ty = mkSpecSigmaTy tvs theta rho + (tvs, theta, rho) = go (dataConUserType data_con) + + go :: Type -> ([TyVar],ThetaType,Type) + -- The returned Type has no foralls or =>, even to the right of an (->) + go ty | null arg_tys = (tvs1, theta1, rho1) + | otherwise = (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) + where + (tvs1, theta1, rho1) = tcSplitNestedSigmaTys ty + (arg_tys, ty2) = tcSplitFunTys rho1 + (tvs2, theta2, rho2) = go ty2 badGadtDecl :: Name -> SDoc badGadtDecl tc_name diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 734ec05512..4c43d91f3e 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -699,8 +699,10 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env -- we did it before the "extra" tvs from etaExpandAlgTyCon -- would always be eta-reduced -- - -- See also Note [Datatype return kinds] in GHC.Tc.TyCl ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind + + -- Check the result kind; it may come from a user-written signature. + -- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a) ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind ; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs all_pats = pats `chkAppend` extra_pats @@ -847,7 +849,8 @@ tcDataFamInstHeader -- Here the "header" is the bit before the "where" tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons new_or_data - = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, lhs_applied_kind))) + = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats) + ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind))) <- pushTcLevelM_ $ solveEqualities $ bindImplicitTKBndrs_Q_Skol imp_vars $ @@ -872,10 +875,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; let lhs_applied_ty = lhs_ty `mkTcAppTys` lhs_extra_args hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind + -- Check that the result kind of the TyCon applied to its args + -- is compatible with the explicit signature (or Type, if there + -- is none) + ; traceTc "tcDataFamInstHeader" $ + vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ] ; return ( stupid_theta , lhs_applied_ty - , lhs_applied_kind ) } + , res_kind ) } -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts] -- This code (and the stuff immediately above) is very similar @@ -888,10 +896,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; qtvs <- quantifyTyVars dvs -- Zonk the patterns etc into the Type world - ; (ze, qtvs) <- zonkTyBndrs qtvs - ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty - ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta - ; lhs_applied_kind <- zonkTcTypeToTypeX ze lhs_applied_kind + ; (ze, qtvs) <- zonkTyBndrs qtvs + ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty + ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta + ; res_kind <- zonkTcTypeToTypeX ze res_kind + + -- We check that res_kind is OK with checkDataKindSig in + -- tcDataFamInstDecl, after eta-expansion. We need to check that + -- it's ok because res_kind can come from a user-written kind signature. + -- See Note [Datatype return kinds], point (4a) -- Check that type patterns match the class instance head -- The call to splitTyConApp_maybe here is just an inlining of @@ -899,7 +912,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; pats <- case splitTyConApp_maybe lhs_ty of Just (_, pats) -> pure pats Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty) - ; return (qtvs, pats, lhs_applied_kind, stupid_theta) } + + ; return (qtvs, pats, res_kind, stupid_theta) } where fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name @@ -920,11 +934,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; lvl <- getTcLevel ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs -- Perhaps surprisingly, we don't need the skolemised tvs themselves - ; let final_kind = substTy subst inner_kind - ; checkDataKindSig (DataInstanceSort new_or_data) $ - snd $ tcSplitPiTys final_kind - -- See Note [Datatype return kinds], end of point (4) - ; return final_kind } + ; return (substTy subst inner_kind) } {- Note [Result kind signature for a data family instance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -932,7 +942,7 @@ The expected type might have a forall at the type. Normally, we can't skolemise in kinds because we don't have type-level lambda. But here, we're at the top-level of an instance declaration, so we actually have a place to put the regeneralised variables. -Thus: skolemise away. cf. Inst.deeplySkolemise and GHC.Tc.Utils.Unify.tcSkolemise +Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcSkolemise Examples in indexed-types/should_compile/T12369 Note [Implementing eta reduction for data families] @@ -1781,7 +1791,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind -- The instance-sig is the focus here; the class-meth-sig -- is fixed (#18036) ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $ - tcSubType_NC ctxt sig_ty local_meth_ty + tcSubTypeSigma ctxt sig_ty local_meth_ty ; return (sig_ty, hs_wrap) } ; inner_meth_name <- newName (nameOccName sel_name) diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 957506c7c5..a785fbbb7a 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -431,9 +431,9 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details = do { -- Look up the variable actually bound by lpat -- and check that it has the expected type arg_id <- tcLookupId arg_name - ; wrap <- tcSubType_NC GenSigCtxt - (idType arg_id) - (substTyUnchecked subst arg_ty) + ; wrap <- tcSubTypeSigma GenSigCtxt + (idType arg_id) + (substTyUnchecked subst arg_ty) -- Why do we need tcSubType here? -- See Note [Pattern synonyms and higher rank types] ; return (mkLHsWrap wrap $ nlHsVar arg_id) } diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 908a23ff26..3f01a7d03a 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -29,7 +29,7 @@ module GHC.Tc.Types.Constraint ( WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, - addInsols, insolublesOnly, addSimples, addImplics, addHole, + addInsols, dropMisleading, addSimples, addImplics, addHoles, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, tyCoVarsOfWCList, insolubleCt, insolubleEqCt, isDroppableCt, insolubleImplic, @@ -961,19 +961,24 @@ addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints addInsols wc cts = wc { wc_simple = wc_simple wc `unionBags` cts } -addHole :: WantedConstraints -> Hole -> WantedConstraints -addHole wc hole - = wc { wc_holes = hole `consBag` wc_holes wc } +addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints +addHoles wc holes + = wc { wc_holes = holes `unionBags` wc_holes wc } -insolublesOnly :: WantedConstraints -> WantedConstraints --- Keep only the definitely-insoluble constraints -insolublesOnly (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) - = WC { wc_simple = filterBag insolubleCt simples - , wc_impl = mapBag implic_insols_only implics +dropMisleading :: WantedConstraints -> WantedConstraints +-- Drop misleading constraints; really just class constraints +-- See Note [Constraints and errors] in GHC.Tc.Utils.Monad +dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) + = WC { wc_simple = filterBag keep_ct simples + , wc_impl = mapBag drop_implic implics , wc_holes = filterBag isOutOfScopeHole holes } where - implic_insols_only implic - = implic { ic_wanted = insolublesOnly (ic_wanted implic) } + drop_implic implic + = implic { ic_wanted = dropMisleading (ic_wanted implic) } + keep_ct ct + = case classifyPredType (ctPred ct) of + ClassPred {} -> False + _ -> True isSolvedStatus :: ImplicStatus -> Bool isSolvedStatus (IC_Solved {}) = True @@ -1100,9 +1105,6 @@ data Implication ic_info :: SkolemInfo, -- See Note [Skolems in an implication] -- See Note [Shadowing in a constraint] - ic_telescope :: Maybe SDoc, -- User-written telescope, if there is one - -- See Note [Checking telescopes] - ic_given :: [EvVar], -- Given evidence variables -- (order does not matter) -- See Invariant (GivenInv) in GHC.Tc.Utils.TcType @@ -1153,7 +1155,6 @@ implicationPrototype -- The rest have sensible default values , ic_skols = [] - , ic_telescope = Nothing , ic_given = [] , ic_wanted = emptyWC , ic_no_eqs = False @@ -1228,17 +1229,18 @@ all at once, creating one implication constraint for the lot: variables (ic_skols). This is done in setImplicationStatus. * This check is only necessary if the implication was born from a - user-written signature. If, say, it comes from checking a pattern - match that binds existentials, where the type of the data constructor - is known to be valid (it in tcConPat), no need for the check. + 'forall' in a user-written signature (the HsForAllTy case in + GHC.Tc.Gen.HsType. If, say, it comes from checking a pattern match + that binds existentials, where the type of the data constructor is + known to be valid (it in tcConPat), no need for the check. - So the check is done if and only if ic_telescope is (Just blah). + So the check is done if and only if ic_info is ForAllSkol -* If ic_telesope is (Just d), the d::SDoc displays the original, - user-written type variables. +* If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the + original, user-written type variables. -* Be careful /NOT/ to discard an implication with non-Nothing - ic_telescope, even if ic_wanted is empty. We must give the +* Be careful /NOT/ to discard an implication with a ForAllSkol + ic_info, even if ic_wanted is empty. We must give the constraint solver a chance to make that bad-telescope test! Hence the extra guard in emitResidualTvConstraint; see #16247 diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 381cdd03ba..b453633c65 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -125,7 +125,7 @@ data UserTypeCtxt pprUserTypeCtxt :: UserTypeCtxt -> SDoc pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n) pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n) -pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n) +pprUserTypeCtxt (RuleSigCtxt n) = text "the type signature for" <+> quotes (ppr n) pprUserTypeCtxt ExprSigCtxt = text "an expression type signature" pprUserTypeCtxt KindSigCtxt = text "a kind signature" pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n) @@ -184,7 +184,10 @@ data SkolemInfo -- like SigSkol, but when we're kind-checking the *type* -- hence, we have less info - | ForAllSkol SDoc -- Bound by a user-written "forall". + | ForAllSkol -- Bound by a user-written "forall". + SDoc -- Shows the entire forall type + SDoc -- Shows just the binders, used when reporting a bad telescope + -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint | DerivSkol Type -- Bound by a 'deriving' clause; -- the type is the instance we are trying to derive @@ -242,7 +245,7 @@ pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty pprSkolInfo (SigTypeSkol cx) = pprUserTypeCtxt cx -pprSkolInfo (ForAllSkol doc) = quotes doc +pprSkolInfo (ForAllSkol pt _) = quotes pt pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for" <+> pprWithCommas ppr ips pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred) @@ -306,8 +309,8 @@ is fine. We could do more, but it doesn't seem worth it. Note [SigSkol SkolemInfo] ~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we (deeply) skolemise a type - f :: forall a. a -> forall b. b -> a +Suppose we skolemise a type + f :: forall a. Eq a => forall b. b -> a Then we'll instantiate [a :-> a', b :-> b'], and with the instantiated a' -> b' -> a. But when, in an error message, we report that "b is a rigid type @@ -321,8 +324,8 @@ in the right place. So we proceed as follows: * Then when tidying in GHC.Tc.Utils.TcMType.tidySkolemInfo, we first tidy a' to whatever it tidies to, say a''; and then we walk over the type replacing the binder a by the tidied version a'', to give - forall a''. a'' -> forall b''. b'' -> a'' - We need to do this under function arrows, to match what deeplySkolemise + forall a''. Eq a'' => forall b''. b'' -> a'' + We need to do this under (=>) arrows, to match what topSkolemise does. * Typically a'' will have a nice pretty name like "a", but the point is diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 8c2a60ba50..2563ff7348 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -593,24 +593,29 @@ tc_extend_local_env top_lvl extra_env thing_inside -- that are bound together with extra_env and should not be regarded -- as free in the types of extra_env. = do { traceTc "tc_extend_local_env" (ppr extra_env) - ; env0 <- getLclEnv - ; let env1 = tcExtendLocalTypeEnv env0 extra_env ; stage <- getStage - ; let env2 = extend_local_env (top_lvl, thLevel stage) extra_env env1 - ; setLclEnv env2 thing_inside } - where - extend_local_env :: (TopLevelFlag, ThLevel) -> [(Name, TcTyThing)] -> TcLclEnv -> TcLclEnv - -- Extend the local LocalRdrEnv and Template Haskell staging env simultaneously - -- Reason for extending LocalRdrEnv: after running a TH splice we need - -- to do renaming. - extend_local_env thlvl pairs env@(TcLclEnv { tcl_rdr = rdr_env - , tcl_th_bndrs = th_bndrs }) - = env { tcl_rdr = extendLocalRdrEnvList rdr_env - [ n | (n, _) <- pairs, isInternalName n ] - -- The LocalRdrEnv contains only non-top-level names - -- (GlobalRdrEnv handles the top level) - , tcl_th_bndrs = extendNameEnvList th_bndrs -- We only track Ids in tcl_th_bndrs - [(n, thlvl) | (n, ATcId {}) <- pairs] } + ; env0@(TcLclEnv { tcl_rdr = rdr_env + , tcl_th_bndrs = th_bndrs + , tcl_env = lcl_type_env }) <- getLclEnv + + ; let thlvl = (top_lvl, thLevel stage) + + env1 = env0 { tcl_rdr = extendLocalRdrEnvList rdr_env + [ n | (n, _) <- extra_env, isInternalName n ] + -- The LocalRdrEnv contains only non-top-level names + -- (GlobalRdrEnv handles the top level) + + , tcl_th_bndrs = extendNameEnvList th_bndrs + [(n, thlvl) | (n, ATcId {}) <- extra_env] + -- We only track Ids in tcl_th_bndrs + + , tcl_env = extendNameEnvList lcl_type_env extra_env } + + -- tcl_rdr and tcl_th_bndrs: extend the local LocalRdrEnv and + -- Template Haskell staging env simultaneously. Reason for extending + -- LocalRdrEnv: after running a TH splice we need to do renaming. + + ; setLclEnv env1 thing_inside } tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcLclEnv tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index ea8ffd912b..df9cf982ee 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -10,10 +10,9 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} --- | The @Inst@ type: dictionaries or method instances module GHC.Tc.Utils.Instantiate ( - deeplySkolemise, - topInstantiate, topInstantiateInferred, deeplyInstantiate, + topSkolemise, + topInstantiate, topInstantiateInferred, instCall, instDFunType, instStupidTheta, instTyVarsWith, newWanted, newWanteds, @@ -36,11 +35,10 @@ module GHC.Tc.Utils.Instantiate ( import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckExpr, tcSyntaxOp ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp ) import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind ) import GHC.Types.Basic ( IntegralLit(..), SourceText(..) ) -import GHC.Data.FastString import GHC.Hs import GHC.Tc.Utils.Zonk import GHC.Tc.Utils.Monad @@ -117,66 +115,62 @@ newMethodFromName origin name ty_args {- ************************************************************************ * * - Deep instantiation and skolemisation + Instantiation and skolemisation * * ************************************************************************ -Note [Deep skolemisation] -~~~~~~~~~~~~~~~~~~~~~~~~~ -deeplySkolemise decomposes and skolemises a type, returning a type -with all its arrows visible (ie not buried under foralls) +Note [Skolemisation] +~~~~~~~~~~~~~~~~~~~~ +topSkolemise decomposes and skolemises a type, returning a type +with no top level foralls or (=>) Examples: - deeplySkolemise (Int -> forall a. Ord a => blah) - = ( wp, [a], [d:Ord a], Int -> blah ) - where wp = \x:Int. /\a. \(d:Ord a). <hole> x + topSkolemise (forall a. Ord a => a -> a) + = ( wp, [a], [d:Ord a], a->a ) + where wp = /\a. \(d:Ord a). <hole> a d - deeplySkolemise (forall a. Ord a => Maybe a -> forall b. Eq b => blah) - = ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah ) - where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x + topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b) + = ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b ) + where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2 + +This second example is the reason for the recursive 'go' +function in topSkolemise: we must remove successive layers +of foralls and (=>). In general, - if deeplySkolemise ty = (wrap, tvs, evs, rho) + if topSkolemise ty = (wrap, tvs, evs, rho) and e :: rho then wrap e :: ty - and 'wrap' binds tvs, evs + and 'wrap' binds {tvs, evs} -ToDo: this eta-abstraction plays fast and loose with termination, - because it can introduce extra lambdas. Maybe add a `seq` to - fix this -} -deeplySkolemise :: TcSigmaType - -> TcM ( HsWrapper - , [(Name,TyVar)] -- All skolemised variables - , [EvVar] -- All "given"s - , TcRhoType ) - -deeplySkolemise ty - = go init_subst ty +topSkolemise :: TcSigmaType + -> TcM ( HsWrapper + , [(Name,TyVar)] -- All skolemised variables + , [EvVar] -- All "given"s + , TcRhoType ) +-- See Note [Skolemisation] +topSkolemise ty + = go init_subst idHsWrapper [] [] ty where init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty)) - go subst ty - | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty - = do { let arg_tys' = substTys subst arg_tys - ; ids1 <- newSysLocalIds (fsLit "dk") arg_tys' - ; (subst', tvs1) <- tcInstSkolTyVarsX subst tvs + -- Why recursive? See Note [Skolemisation] + go subst wrap tv_prs ev_vars ty + | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (subst', tvs1) <- tcInstSkolTyVarsX subst tvs ; ev_vars1 <- newEvVars (substTheta subst' theta) - ; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty' - ; let tv_prs1 = map tyVarName tvs `zip` tvs1 - ; return ( mkWpLams ids1 - <.> mkWpTyLams tvs1 - <.> mkWpLams ev_vars1 - <.> wrap - <.> mkWpEvVarApps ids1 - , tv_prs1 ++ tvs_prs2 - , ev_vars1 ++ ev_vars2 - , mkVisFunTys arg_tys' rho ) } + ; go subst' + (wrap <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1) + (tv_prs ++ (map tyVarName tvs `zip` tvs1)) + (ev_vars ++ ev_vars1) + inner_ty } | otherwise - = return (idHsWrapper, [], [], substTy subst ty) + = return (wrap, tv_prs, ev_vars, substTy subst ty) -- substTy is a quick no-op on an empty substitution -- | Instantiate all outer type variables @@ -185,6 +179,7 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- if topInstantiate ty = (wrap, rho) -- 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 -- | Instantiate all outer 'Inferred' binders @@ -195,13 +190,16 @@ topInstantiateInferred :: CtOrigin -> 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 - | not (null binders && null theta) + | (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, []) @@ -226,7 +224,7 @@ top_instantiate inst_all orig ty , text "theta:" <+> ppr inst_theta' ]) ; (wrap2, rho2) <- - if null leave_bndrs + if null leave_bndrs -- NB: if inst_all is True then leave_bndrs = [] -- account for types like forall a. Num a => forall b. Ord b => ... then top_instantiate inst_all orig sigma' @@ -238,67 +236,11 @@ top_instantiate inst_all orig ty | otherwise = return (idHsWrapper, ty) where - (binders, phi) = tcSplitForAllVarBndrs ty - (theta, rho) = tcSplitPhiTy phi should_inst bndr | inst_all = True | otherwise = binderArgFlag bndr == Inferred -deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) --- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha --- In general if --- if deeplyInstantiate ty = (wrap, rho) --- and e :: ty --- then wrap e :: rho --- That is, wrap :: ty ~> rho --- --- If you don't need the HsWrapper returned from this function, consider --- using tcSplitNestedSigmaTys in GHC.Tc.Utils.TcType, which is a pure alternative that --- only computes the returned TcRhoType. - -deeplyInstantiate orig ty = - deeply_instantiate orig - (mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))) - ty - -deeply_instantiate :: CtOrigin - -> TCvSubst - -> TcSigmaType -> TcM (HsWrapper, TcRhoType) --- Internal function to deeply instantiate that builds on an existing subst. --- It extends the input substitution and applies the final substitution to --- the types on return. See #12549. - -deeply_instantiate orig subst ty - | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty - = do { (subst', tvs') <- newMetaTyVarsX subst tvs - ; let arg_tys' = substTys subst' arg_tys - theta' = substTheta subst' theta - ; ids1 <- newSysLocalIds (fsLit "di") arg_tys' - ; wrap1 <- instCall orig (mkTyVarTys tvs') theta' - ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig - , text "type" <+> ppr ty - , text "with" <+> ppr tvs' - , text "args:" <+> ppr ids1 - , text "theta:" <+> ppr theta' - , text "subst:" <+> ppr subst']) - ; (wrap2, rho2) <- deeply_instantiate orig subst' rho - ; return (mkWpLams ids1 - <.> wrap2 - <.> wrap1 - <.> mkWpEvVarApps ids1, - mkVisFunTys arg_tys' rho2) } - - | otherwise - = do { let ty' = substTy subst ty - ; traceTc "deeply_instantiate final subst" - (vcat [ text "origin:" <+> pprCtOrigin orig - , text "type:" <+> ppr ty - , text "new type:" <+> ppr ty' - , text "subst:" <+> ppr subst ]) - ; return (idHsWrapper, ty') } - - instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst -- Use this when you want to instantiate (forall a b c. ty) with -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might @@ -639,7 +581,7 @@ tcSyntaxName orig ty (std_nm, user_nm_expr) = do -- same type as the standard one. -- Tiresome jiggling because tcCheckSigma takes a located expression span <- getSrcSpanM - expr <- tcCheckExpr (L span user_nm_expr) sigma1 + expr <- tcCheckPolyExpr (L span user_nm_expr) sigma1 return (std_nm, unLoc expr) syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 2fc741ce6f..d7fbd2e095 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -98,7 +98,8 @@ module GHC.Tc.Utils.Monad( chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitStaticConstraints, emitSimple, emitSimples, - emitImplication, emitImplications, emitInsoluble, emitHole, + emitImplication, emitImplications, emitInsoluble, + emitHole, emitHoles, discardConstraints, captureConstraints, tryCaptureConstraints, pushLevelAndCaptureConstraints, pushTcLevelM_, pushTcLevelM, pushTcLevelsM, @@ -1145,7 +1146,7 @@ askNoErrs thing_inside ; addMessages msgs ; case mb_res of - Nothing -> do { emitConstraints (insolublesOnly lie) + Nothing -> do { emitConstraints (dropMisleading lie) ; failM } Just res -> do { emitConstraints lie @@ -1167,7 +1168,7 @@ tryCaptureConstraints thing_inside -- See Note [Constraints and errors] ; let lie_to_keep = case mb_res of - Nothing -> insolublesOnly lie + Nothing -> dropMisleading lie Just {} -> lie ; return (mb_res, lie_to_keep) } @@ -1589,7 +1590,13 @@ emitHole :: Hole -> TcM () emitHole hole = do { traceTc "emitHole" (ppr hole) ; lie_var <- getConstraintVar - ; updTcRef lie_var (`addHole` hole) } + ; updTcRef lie_var (`addHoles` unitBag hole) } + +emitHoles :: Bag Hole -> TcM () +emitHoles holes + = do { traceTc "emitHoles" (ppr holes) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addHoles` holes) } -- | Throw out any constraints emitted by the thing_inside discardConstraints :: TcM a -> TcM a diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index d06307263d..97267a8641 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -27,7 +27,8 @@ module GHC.Tc.Utils.TcMType ( newFmvTyVar, newFskTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, - newMetaDetails, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, + newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName, + isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- -- Expected types @@ -70,7 +71,7 @@ module GHC.Tc.Utils.TcMType ( zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, tidyEvVar, tidyCt, tidyHole, tidySkolemInfo, zonkTcTyVar, zonkTcTyVars, - zonkTcTyVarToTyVar, zonkTyVarTyVarPairs, + zonkTcTyVarToTyVar, zonkInvisTVBinder, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV, zonkTyCoVarsAndFVList, candidateQTyVarsOfType, candidateQTyVarsOfKind, @@ -81,7 +82,7 @@ module GHC.Tc.Utils.TcMType ( zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, zonkTyCoVarKindBinder, - zonkEvVar, zonkWC, zonkSimples, + zonkEvVar, zonkWC, zonkImplication, zonkSimples, zonkId, zonkCoVar, zonkCt, zonkSkolemInfo, @@ -119,7 +120,6 @@ import GHC.Builtin.Types import GHC.Builtin.Types.Prim import GHC.Types.Var.Env import GHC.Types.Name.Env -import GHC.Builtin.Names import GHC.Utils.Misc import GHC.Utils.Outputable import GHC.Data.FastString @@ -144,18 +144,13 @@ import qualified Data.Semigroup as Semi ************************************************************************ -} -mkKindName :: Unique -> Name -mkKindName unique = mkSystemName unique kind_var_occ - -kind_var_occ :: OccName -- Just one for all MetaKindVars - -- They may be jiggled by tidying -kind_var_occ = mkOccName tvName "k" - newMetaKindVar :: TcM TcKind newMetaKindVar = do { details <- newMetaDetails TauTv - ; uniq <- newUnique - ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details + ; name <- newMetaTyVarName (fsLit "k") + -- All MetaKindVars are called "k" + -- They may be jiggled by tidying + ; let kv = mkTcTyVar name liftedTypeKind details ; traceTc "newMetaKindVar" (ppr kv) ; return (mkTyVarTy kv) } @@ -834,6 +829,13 @@ newMetaDetails info , mtv_ref = ref , mtv_tclvl = tclvl }) } +newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails +newTauTvDetailsAtLevel tclvl + = do { ref <- newMutVar Flexi + ; return (MetaTv { mtv_info = TauTv + , mtv_ref = ref + , mtv_tclvl = tclvl }) } + cloneMetaTyVar :: TcTyVar -> TcM TcTyVar cloneMetaTyVar tv = ASSERT( isTcTyVar tv ) @@ -1060,18 +1062,15 @@ new_meta_tv_x info subst tv -- is not yet fixed so leaving as unchecked for now. -- OLD NOTE: -- Unchecked because we call newMetaTyVarX from - -- tcInstTyBinder, which is called from tcInferApps + -- tcInstTyBinder, which is called from tcInferTyApps -- which does not yet take enough trouble to ensure -- the in-scope set is right; e.g. #12785 trips -- if we use substTy here newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType newMetaTyVarTyAtLevel tc_lvl kind - = do { ref <- newMutVar Flexi - ; name <- newMetaTyVarName (fsLit "p") - ; let details = MetaTv { mtv_info = TauTv - , mtv_ref = ref - , mtv_tclvl = tc_lvl } + = do { details <- newTauTvDetailsAtLevel tc_lvl + ; name <- newMetaTyVarName (fsLit "p") ; return (mkTyVarTy (mkTcTyVar name kind details)) } {- ********************************************************************* @@ -1254,13 +1253,14 @@ instance Outputable CandidatesQTvs where candidateKindVars :: CandidatesQTvs -> TyVarSet candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) -partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (DTyVarSet, CandidatesQTvs) +partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs) +-- The selected TyVars are returned as a non-deterministic TyVarSet partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs }) where (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs - extracted = extracted_kvs `unionDVarSet` extracted_tvs + extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs -- | Gathers free variables to use as quantification candidates (in -- 'quantifyTyVars'). This might output the same var @@ -2218,12 +2218,9 @@ zonkTcTyVarToTyVar tv (ppr tv $$ ppr ty) ; return tv' } -zonkTyVarTyVarPairs :: [(Name,VarBndr TcTyVar Specificity)] -> TcM [(Name,VarBndr TcTyVar Specificity)] -zonkTyVarTyVarPairs prs - = mapM do_one prs - where - do_one (nm, Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv - ; return (nm, Bndr tv' spec) } +zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TyVar spec) +zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv + ; return (Bndr tv' spec) } -- zonkId is used *during* typechecking just to zonk the Id's type zonkId :: TcId -> TcM TcId @@ -2342,7 +2339,7 @@ tidySigSkol env cx ty tv_prs where (env', tv') = tidy_tv_bndr env tv - tidy_ty env ty@(FunTy _ arg res) + tidy_ty env ty@(FunTy InvisArg arg res) -- Look under c => t = ty { ft_arg = tidyType env arg, ft_res = tidy_ty env res } tidy_ty env ty = tidyType env ty diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index fb1d6f432b..c1d7af0120 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -67,7 +67,7 @@ module GHC.Tc.Utils.TcType ( tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe, tcRepGetNumAppTys, tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, - tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe, + tcSplitSigmaTy, tcSplitNestedSigmaTys, --------------------------------- -- Predicates. @@ -412,7 +412,7 @@ mkCheckExpType = Check -- This is defined here to avoid defining it in GHC.Tc.Gen.Expr boot file. data SyntaxOpType = SynAny -- ^ Any type - | SynRho -- ^ A rho type, deeply skolemised or instantiated as appropriate + | SynRho -- ^ A rho type, skolemised or instantiated as appropriate | SynList -- ^ A list type. You get back the element type of the list | SynFun SyntaxOpType SyntaxOpType -- ^ A function. @@ -431,11 +431,12 @@ mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys {- Note [TcRhoType] ~~~~~~~~~~~~~~~~ -A TcRhoType has no foralls or contexts at the top, or to the right of an arrow - YES (forall a. a->a) -> Int +A TcRhoType has no foralls or contexts at the top NO forall a. a -> Int NO Eq a => a -> a - NO Int -> forall a. a -> Int + YES a -> a + YES (forall a. a->a) -> Int + YES Int -> forall a. a -> Int ************************************************************************ @@ -1273,35 +1274,19 @@ tcSplitSigmaTy ty = case tcSplitForAllTys ty of -- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return -- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@. tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type) --- NB: This is basically a pure version of deeplyInstantiate (from Inst) that +-- NB: This is basically a pure version of topInstantiate (from Inst) that -- doesn't compute an HsWrapper. tcSplitNestedSigmaTys ty -- If there's a forall, split it apart and try splitting the rho type -- underneath it. - | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty + | (tvs1, theta1, rho1) <- tcSplitSigmaTy ty + , not (null tvs1 && null theta1) = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1 - in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) + in (tvs1 ++ tvs2, theta1 ++ theta2, rho2) -- If there's no forall, we're done. | otherwise = ([], [], ty) ----------------------- -tcDeepSplitSigmaTy_maybe - :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType) --- Looks for a *non-trivial* quantified type, under zero or more function arrows --- By "non-trivial" we mean either tyvars or constraints are non-empty - -tcDeepSplitSigmaTy_maybe ty - | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty - , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty - = Just (arg_ty:arg_tys, tvs, theta, rho) - - | (tvs, theta, rho) <- tcSplitSigmaTy ty - , not (null tvs && null theta) - = Just ([], tvs, theta, rho) - - | otherwise = Nothing - ------------------------ tcTyConAppTyCon :: Type -> TyCon tcTyConAppTyCon ty = case tcTyConAppTyCon_maybe ty of @@ -1997,9 +1982,9 @@ isSigmaTy _ = False isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType] isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty' -isRhoTy (ForAllTy {}) = False -isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r -isRhoTy _ = True +isRhoTy (ForAllTy {}) = False +isRhoTy (FunTy { ft_af = InvisArg }) = False +isRhoTy _ = True -- | Like 'isRhoTy', but also says 'True' for 'Infer' types isRhoExpTy :: ExpType -> Bool diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 7c14e56319..8ca3ae7723 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -13,11 +13,11 @@ -- | Type subsumption and unification module GHC.Tc.Utils.Unify ( -- Full-blown subsumption - tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, - tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, - tcSubTypeDS_NC_O, tcSubTypePat, + tcWrapResult, tcWrapResultO, tcWrapResultMono, + tcSkolemise, tcSkolemiseScoped, tcSkolemiseET, + tcSubType, tcSubTypeSigma, tcSubTypePat, checkConstraints, checkTvConstraints, - buildImplicationFor, emitResidualTvConstraint, + buildImplicationFor, buildTvImplication, emitResidualTvConstraint, -- Various unifications unifyType, unifyKind, @@ -31,7 +31,7 @@ module GHC.Tc.Utils.Unify ( matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, - matchActualFunTys, matchActualFunTysPart, + matchActualFunTysRho, matchActualFunTySigma, matchExpectedFunKind, metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) @@ -48,6 +48,7 @@ import GHC.Core.TyCo.Ppr( debugPprType ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Env import GHC.Core.Type import GHC.Core.Coercion import GHC.Tc.Types.Evidence @@ -70,7 +71,6 @@ import GHC.Utils.Misc import qualified GHC.LanguageExtensions as LangExt import GHC.Utils.Outputable as Outputable -import Data.Maybe( isNothing ) import Control.Monad import Control.Arrow ( second ) @@ -139,34 +139,46 @@ passed in. -} -- Use this one when you have an "expected" type. +-- This function skolemises at each polytype. matchExpectedFunTys :: forall a. SDoc -- See Note [Herald for matchExpectedFunTys] + -> UserTypeCtxt -> Arity - -> ExpRhoType -- deeply skolemised + -> ExpRhoType -- Skolemised -> ([ExpSigmaType] -> ExpRhoType -> TcM a) - -- must fill in these ExpTypes here - -> TcM (a, HsWrapper) + -> TcM (HsWrapper, a) -- If matchExpectedFunTys n ty = (_, wrap) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside -matchExpectedFunTys herald arity orig_ty thing_inside +matchExpectedFunTys herald ctx arity orig_ty thing_inside = case orig_ty of Check ty -> go [] arity ty _ -> defer [] arity orig_ty where - go acc_arg_tys 0 ty - = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty) - ; return (result, idHsWrapper) } + -- Skolemise any foralls /before/ the zero-arg case + -- so that we guarantee to return a rho-type + go acc_arg_tys n ty + | (tvs, theta, _) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' -> + go acc_arg_tys n ty' + ; return (wrap_gen <.> wrap_res, result) } + + -- No more args; do this /before/ tcView, so + -- that we do not unnecessarily unwrap synonyms + go acc_arg_tys 0 rho_ty + = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty) + ; return (idHsWrapper, result) } go acc_arg_tys n ty | Just ty' <- tcView ty = go acc_arg_tys n ty' go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys) + do { (wrap_res, result) <- go (mkCheckExpType arg_ty : acc_arg_tys) (n-1) res_ty - ; return ( result - , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) } + ; let fun_wrap = mkWpFun idHsWrapper wrap_res arg_ty res_ty doc + ; return ( fun_wrap, result ) } where doc = text "When inferring the argument type of a function with type" <+> quotes (ppr orig_ty) @@ -197,7 +209,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ - defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper) + defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty = do { more_arg_tys <- replicateM n newInferExpType ; res_ty <- newInferExpType @@ -205,9 +217,9 @@ matchExpectedFunTys herald arity orig_ty thing_inside ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty - ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty + ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty -- Not a good origin at all :-( - ; return (result, wrap) } + ; return (wrap, result) } ------------ mk_ctxt :: [ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) @@ -220,36 +232,54 @@ matchExpectedFunTys herald arity orig_ty thing_inside -- Like 'matchExpectedFunTys', but used when you have an "actual" type, -- for example in function application -matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType - -> Arity - -> TcSigmaType - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) --- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) --- then wrap : ty ~> (t1 -> ... -> tn -> ty_r) -matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty - = matchActualFunTysPart herald ct_orig mb_thing - n_val_args_wanted [] - n_val_args_wanted fun_ty - --- | Variant of 'matchActualFunTys' that works when supplied only part --- (that is, to the right of some arrows) of the full function type -matchActualFunTysPart +matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType + -> Arity + -> TcSigmaType + -> TcM (HsWrapper, [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 -- Total number of value args in the call - -> [TcSigmaType] -- Types of values args to which function has - -- been applied already (reversed) - -> Arity -- Number of new value args wanted - -> TcSigmaType -- Type to analyse - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) + -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType + -> (Arity, [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, TcSigmaType, TcSigmaType) -- See Note [matchActualFunTys error handling] for all these arguments -matchActualFunTysPart herald ct_orig mb_thing - n_val_args_in_call arg_tys_so_far - n_val_args_wanted fun_ty - = go n_val_args_wanted arg_tys_so_far fun_ty + +-- 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 @@ -264,52 +294,28 @@ matchActualFunTysPart herald ct_orig mb_thing -- in elsewhere). where - -- This function has a bizarre mechanic: it accumulates arguments on - -- the way down and also builds an argument list on the way up. Why: - -- 1. The returns args list and the accumulated args list might be different. - -- The accumulated args include all the arg types for the function, - -- including those from before this function was called. The returned - -- list should include only those arguments produced by this call of - -- matchActualFunTys - -- - -- 2. The HsWrapper can be built only on the way up. It seems (more) - -- bizarre to build the HsWrapper but not the arg_tys. - -- - -- Refactoring is welcome. - go :: Arity - -> [TcSigmaType] -- Types of value args to which the function has - -- been applied so far (reversed) - -- Used only for error messages - -> TcSigmaType -- the remainder of the type as we're processing - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) - go 0 _ ty = return (idHsWrapper, [], ty) - - go n so_far ty + go :: TcSigmaType -- The remainder of the type as we're processing + -> TcM (HsWrapper, TcSigmaType, TcSigmaType) + go ty | Just ty' <- tcView ty = go ty' + + go ty | not (null tvs && null theta) = do { (wrap1, rho) <- topInstantiate ct_orig ty - ; (wrap2, arg_tys, res_ty) <- go n so_far rho - ; return (wrap2 <.> wrap1, arg_tys, res_ty) } + ; (wrap2, arg_ty, res_ty) <- go rho + ; return (wrap2 <.> wrap1, arg_ty, res_ty) } where (tvs, theta, _) = tcSplitSigmaTy ty - go n so_far ty - | Just ty' <- tcView ty = go n so_far ty' - - go n so_far (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) + go (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty:so_far) res_ty - ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc - , arg_ty : tys, ty_r ) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr fun_ty) + return (idHsWrapper, arg_ty, res_ty) - go n so_far ty@(TyVarTy tv) + go ty@(TyVarTy tv) | isMetaTyVar tv = do { cts <- readMetaTyVar tv ; case cts of - Indirect ty' -> go n so_far ty' - Flexi -> defer n ty } + 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 @@ -326,22 +332,23 @@ matchActualFunTysPart herald ct_orig mb_thing -- -- But in that case we add specialized type into error context -- anyway, because it may be useful. See also #9605. - go n so_far ty = addErrCtxtM (mk_ctxt so_far ty) (defer n ty) + go ty = addErrCtxtM (mk_ctxt ty) (defer ty) ------------ - defer n fun_ty - = do { arg_tys <- replicateM n newOpenFlexiTyVarTy - ; res_ty <- newOpenFlexiTyVarTy - ; let unif_fun_ty = mkVisFunTys arg_tys res_ty + defer fun_ty + = do { arg_ty <- newOpenFlexiTyVarTy + ; res_ty <- newOpenFlexiTyVarTy + ; let unif_fun_ty = mkVisFunTy arg_ty res_ty ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; return (mkWpCastN co, arg_tys, res_ty) } + ; return (mkWpCastN co, arg_ty, res_ty) } ------------ - mk_ctxt :: [TcType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt arg_tys res_ty env + mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt res_ty env = do { (env', ty) <- zonkTidyTcType env $ - mkVisFunTys (reverse arg_tys) res_ty + 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 @@ -491,95 +498,51 @@ a place expecting a value of type expected_ty. I.e. that actual ty is more polymorphic than expected_ty -It returns a coercion function +It returns a wrapper function co_fn :: actual_ty ~ expected_ty which takes an HsExpr of type actual_ty into one of type expected_ty. - -These functions do not actually check for subsumption. They check if -expected_ty is an appropriate annotation to use for something of type -actual_ty. This difference matters when thinking about visible type -application. For example, - - forall a. a -> forall b. b -> b - DOES NOT SUBSUME - forall a b. a -> b -> b - -because the type arguments appear in a different order. (Neither does -it work the other way around.) BUT, these types are appropriate annotations -for one another. Because the user directs annotations, it's OK if some -arguments shuffle around -- after all, it's what the user wants. -Bottom line: none of this changes with visible type application. - -There are a number of wrinkles (below). - -Notice that Wrinkle 1 and 2 both require eta-expansion, which technically -may increase termination. We just put up with this, in exchange for getting -more predictable type inference. - -Wrinkle 1: Note [Deep skolemisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a) -(see section 4.6 of "Practical type inference for higher rank types") -So we must deeply-skolemise the RHS before we instantiate the LHS. - -That is why tc_sub_type starts with a call to tcSkolemise (which does the -deep skolemisation), and then calls the DS variant (which assumes -that expected_ty is deeply skolemised) - -Wrinkle 2: Note [Co/contra-variance of subsumption checking] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider g :: (Int -> Int) -> Int - f1 :: (forall a. a -> a) -> Int - f1 = g - - f2 :: (forall a. a -> a) -> Int - f2 x = g x -f2 will typecheck, and it would be odd/fragile if f1 did not. -But f1 will only typecheck if we have that - (Int->Int) -> Int <= (forall a. a->a) -> Int -And that is only true if we do the full co/contravariant thing -in the subsumption check. That happens in the FunTy case of -tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of -HsWrapper. - -Another powerful reason for doing this co/contra stuff is visible -in #9569, involving instantiation of constraint variables, -and again involving eta-expansion. - -Wrinkle 3: Note [Higher rank types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider tc150: - f y = \ (x::forall a. a->a). blah -The following happens: -* We will infer the type of the RHS, ie with a res_ty = alpha. -* Then the lambda will split alpha := beta -> gamma. -* And then we'll check tcSubType IsSwapped beta (forall a. a->a) - -So it's important that we unify beta := forall a. a->a, rather than -skolemising the type. -} --- | Call this variant when you are in a higher-rank situation and --- you know the right-hand type is deeply skolemised. -tcSubTypeHR :: CtOrigin -- ^ of the actual type - -> Maybe (HsExpr GhcRn) -- ^ If present, it has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt +----------------- +-- tcWrapResult needs both un-type-checked (for origins and error messages) +-- and type-checked (for wrapping) expressions +tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType + -> TcM (HsExpr GhcTcId) +tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr + +tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType + -> TcM (HsExpr GhcTcId) +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 + ; return (mkHsWrap wrap expr) } + +tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTcId + -> TcRhoType -- Actual -- a rho-type not a sigma-type + -> ExpRhoType -- Expected + -> TcM (HsExpr GhcTcId) +-- A version of tcWrapResult to use when the actual type is a +-- rho-type, so nothing to instantiate; just go straight to unify. +-- It means we don't need to pass in a CtOrigin +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 + ; return (mkHsWrapCo co expr) } ------------------------ tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper +-- Used in patterns; polarity is backwards compared +-- to tcSubType -- If wrap = tc_sub_type_et t1 t2 -- => wrap :: t1 ~> t2 -tcSubTypePat orig ctxt (Check ty_actual) ty_expected - = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected - where - eq_orig = TypeEqOrigin { uo_actual = ty_expected - , uo_expected = ty_actual - , uo_thing = Nothing - , uo_visible = True } +tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected + = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected tcSubTypePat _ _ (Infer inf_res) ty_expected = do { co <- fillInferResult ty_expected inf_res @@ -587,106 +550,72 @@ tcSubTypePat _ _ (Infer inf_res) ty_expected ; return (mkWpCastN (mkTcSymCo co)) } ------------------------- -tcSubTypeO :: CtOrigin -- ^ of the actual type - -> UserTypeCtxt -- ^ of the expected type - -> TcSigmaType - -> ExpRhoType - -> TcM HsWrapper -tcSubTypeO orig ctxt ty_actual ty_expected +--------------- +tcSubType :: CtOrigin -> UserTypeCtxt + -> TcSigmaType -- Actual + -> ExpRhoType -- Expected + -> TcM HsWrapper +-- Checks that 'actual' is more polymorphic than 'expected' +tcSubType orig ctxt ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig - , pprUserTypeCtxt ctxt - , ppr ty_actual - , ppr ty_expected ]) - ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } - -addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a -addSubTypeCtxt ty_actual ty_expected thing_inside - | isRhoTy ty_actual -- If there is no polymorphism involved, the - , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions) - = thing_inside -- gives enough context by itself - | otherwise - = addErrCtxtM mk_msg thing_inside - where - mk_msg tidy_env - = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual - -- might not be filled if we're debugging. ugh. - ; mb_ty_expected <- readExpType_maybe ty_expected - ; (tidy_env, ty_expected) <- case mb_ty_expected of - Just ty -> second mkCheckExpType <$> - zonkTidyTcType tidy_env ty - Nothing -> return (tidy_env, ty_expected) - ; ty_expected <- readExpType ty_expected - ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected - ; let msg = vcat [ hang (text "When checking that:") - 4 (ppr ty_actual) - , nest 2 (hang (text "is more polymorphic than:") - 2 (ppr ty_expected)) ] - ; return (tidy_env, msg) } + do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) + ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected } + +tcSubTypeNC :: CtOrigin -- Used when instantiating + -> UserTypeCtxt -- Used when skolemising + -> Maybe (HsExpr GhcRn) -- The expression that has type 'actual' (if known) + -> TcSigmaType -- Actual type + -> ExpRhoType -- Expected type + -> TcM HsWrapper +tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty + = case res_ty of + Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res + Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt + ty_actual ty_expected --------------- --- The "_NC" variants do not add a typechecker-error context; --- the caller is assumed to do that - -tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- External entry point, but no ExpTypes on either side -- Checks that actual <= expected -- Returns HsWrapper :: actual ~ expected -tcSubType_NC ctxt ty_actual ty_expected - = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected } +tcSubTypeSigma ctxt ty_actual ty_expected + = tc_sub_type (unifyType Nothing) eq_orig ctxt ty_actual ty_expected where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = Nothing - , uo_visible = True } - -tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised (hence "DS") -tcSubTypeDS orig ctxt ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } - -tcSubTypeDS_NC_O :: CtOrigin -- origin used for instantiation only - -> UserTypeCtxt - -> Maybe (HsExpr GhcRn) - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised -tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected - = case ty_expected of - Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res - Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty - where - eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty - , uo_thing = ppr <$> m_thing - , uo_visible = True } + eq_orig = TypeEqOrigin { uo_actual = ty_actual + , uo_expected = ty_expected + , uo_thing = Nothing + , uo_visible = True } --------------- -tc_sub_tc_type :: CtOrigin -- used when calling uType - -> CtOrigin -- used when instantiating - -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify + -> CtOrigin -- Used when instantiating + -> UserTypeCtxt -- Used when skolemising + -> TcSigmaType -- Actual; a sigma-type + -> TcSigmaType -- Expected; also a sigma-type + -> TcM HsWrapper +-- Checks that actual_ty is more polymorphic than expected_ty -- If wrap = tc_sub_type t1 t2 -- => wrap :: t1 ~> t2 -tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected +tc_sub_type unify inst_orig ctxt ty_actual ty_expected | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily] , not (possibly_poly ty_actual) - = do { traceTc "tc_sub_tc_type (drop to equality)" $ + = do { traceTc "tc_sub_type (drop to equality)" $ vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] ; mkWpCastN <$> - uType TypeLevel eq_orig ty_actual ty_expected } + unify ty_actual ty_expected } | otherwise -- This is the general case - = do { traceTc "tc_sub_tc_type (general case)" $ + = do { traceTc "tc_sub_type (general case)" $ vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] - ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ - \ _ sk_rho -> - tc_sub_type_ds eq_orig inst_orig ctxt - ty_actual sk_rho + + ; (sk_wrap, inner_wrap) + <- tcSkolemise ctxt ty_expected $ \ sk_rho -> + do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual + ; cow <- unify rho_a sk_rho + ; return (mkWpCastN cow <.> wrap) } + ; return (sk_wrap <.> inner_wrap) } where possibly_poly ty @@ -705,6 +634,31 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected | otherwise = False +------------------------ +addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a +addSubTypeCtxt ty_actual ty_expected thing_inside + | isRhoTy ty_actual -- If there is no polymorphism involved, the + , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions) + = thing_inside -- gives enough context by itself + | otherwise + = addErrCtxtM mk_msg thing_inside + where + mk_msg tidy_env + = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual + -- might not be filled if we're debugging. ugh. + ; mb_ty_expected <- readExpType_maybe ty_expected + ; (tidy_env, ty_expected) <- case mb_ty_expected of + Just ty -> second mkCheckExpType <$> + zonkTidyTcType tidy_env ty + Nothing -> return (tidy_env, ty_expected) + ; ty_expected <- readExpType ty_expected + ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected + ; let msg = vcat [ hang (text "When checking that:") + 4 (ppr ty_actual) + , nest 2 (hang (text "is more polymorphic than:") + 2 (ppr ty_expected)) ] + ; return (tidy_env, msg) } + {- Note [Don't skolemise unnecessarily] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are trying to solve @@ -740,98 +694,9 @@ accept (e.g. #13752). So the test (which is only to improve error message) is very conservative: * ty_actual is /definitely/ monomorphic * ty_expected is /definitely/ polymorphic --} - ---------------- -tc_sub_type_ds :: CtOrigin -- used when calling uType - -> CtOrigin -- used when instantiating - -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper --- If wrap = tc_sub_type_ds t1 t2 --- => wrap :: t1 ~> t2 --- Here is where the work actually happens! --- Precondition: ty_expected is deeply skolemised -tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected - = do { traceTc "tc_sub_type_ds" $ - vcat [ text "ty_actual =" <+> ppr ty_actual - , text "ty_expected =" <+> ppr ty_expected ] - ; go ty_actual ty_expected } - where - go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e - | Just ty_e' <- tcView ty_e = go ty_a ty_e' - go (TyVarTy tv_a) ty_e - = do { lookup_res <- lookupTcTyVar tv_a - ; case lookup_res of - Filled ty_a' -> - do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:" - (ppr tv_a <+> text "-->" <+> ppr ty_a') - ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e } - Unfilled _ -> unify } - - -- Historical note (Sept 16): there was a case here for - -- go ty_a (TyVarTy alpha) - -- which, in the impredicative case unified alpha := ty_a - -- where th_a is a polytype. Not only is this probably bogus (we - -- simply do not have decent story for impredicative types), but it - -- caused #12616 because (also bizarrely) 'deriving' code had - -- -XImpredicativeTypes on. I deleted the entire case. - - go (FunTy { ft_af = VisArg, ft_arg = act_arg, ft_res = act_res }) - (FunTy { ft_af = VisArg, ft_arg = exp_arg, ft_res = exp_res }) - = -- See Note [Co/contra-variance of subsumption checking] - do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res - ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg - -- GenSigCtxt: See Note [Setting the argument context] - ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) } - -- arg_wrap :: exp_arg ~> act_arg - -- res_wrap :: act-res ~> exp_res - where - given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg []) - doc = text "When checking that" <+> quotes (ppr ty_actual) <+> - text "is more polymorphic than" <+> quotes (ppr ty_expected) - - go ty_a ty_e - | let (tvs, theta, _) = tcSplitSigmaTy ty_a - , not (null tvs && null theta) - = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a - ; body_wrap <- tc_sub_type_ds - (eq_orig { uo_actual = in_rho - , uo_expected = ty_expected }) - inst_orig ctxt in_rho ty_e - ; return (body_wrap <.> in_wrap) } - - | otherwise -- Revert to unification - = inst_and_unify - -- It's still possible that ty_actual has nested foralls. Instantiate - -- these, as there's no way unification will succeed with them in. - -- See typecheck/should_compile/T11305 for an example of when this - -- is important. The problem is that we're checking something like - -- a -> forall b. b -> b <= alpha beta gamma - -- where we end up with alpha := (->) - - inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual - - -- If we haven't recurred through an arrow, then - -- the eq_orig will list ty_actual. In this case, - -- we want to update the origin to reflect the - -- instantiation. If we *have* recurred through - -- an arrow, it's better not to update. - ; let eq_orig' = case eq_orig of - TypeEqOrigin { uo_actual = orig_ty_actual } - | orig_ty_actual `tcEqType` ty_actual - , not (isIdHsWrapper wrap) - -> eq_orig { uo_actual = rho_a } - _ -> eq_orig - - ; cow <- uType TypeLevel eq_orig' rho_a ty_expected - ; return (mkWpCastN cow <.> wrap) } - - - -- use versions without synonyms expanded - unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected - -{- Note [Settting the argument context] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Settting the argument context] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider we are doing the ambiguity check for the (bogus) f :: (forall a b. C b => a -> a) -> Int @@ -857,24 +722,6 @@ to a UserTypeCtxt of GenSigCtxt. Why? See Note [When to build an implication] -} ------------------ --- needs both un-type-checked (for origins) and type-checked (for wrapping) --- expressions -tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType - -> TcM (HsExpr GhcTcId) -tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr - --- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more --- convenient. -tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType - -> TcM (HsExpr GhcTcId) -tcWrapResultO orig rn_expr expr actual_ty res_ty - = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty - , text "Expected:" <+> ppr res_ty ]) - ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt - (Just rn_expr) actual_ty res_ty - ; return (mkHsWrap cow expr) } - {- ********************************************************************** %* * @@ -896,7 +743,7 @@ instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrap -- => wrap :: t1 ~> t2 -- See Note [Instantiation of InferResult] instantiateAndFillInferResult orig ty inf_res - = do { (wrap, rho) <- deeplyInstantiate orig ty + = do { (wrap, rho) <- topInstantiate orig ty ; co <- fillInferResult rho inf_res ; return (mkWpCastN co <.> wrap) } @@ -1090,48 +937,64 @@ the thinking. * * ********************************************************************* -} --- | Take an "expected type" and strip off quantifiers to expose the --- type underneath, binding the new skolems for the @thing_inside@. --- The returned 'HsWrapper' has type @specific_ty -> expected_ty@. -tcSkolemise :: UserTypeCtxt -> TcSigmaType - -> ([TcTyVar] -> TcType -> TcM result) - -- ^ These are only ever used for scoped type variables. - -> TcM (HsWrapper, result) - -- ^ The expression has type: spec_ty -> expected_ty +{- Note [Skolemisation] +~~~~~~~~~~~~~~~~~~~~~~~ +tcSkolemise takes "expected type" and strip off quantifiers to expose the +type underneath, binding the new skolems for the 'thing_inside' +The returned 'HsWrapper' has type (specific_ty -> expected_ty). + +Note that for a nested type like + forall a. Eq a => forall b. Ord b => blah +we still only build one implication constraint + forall a b. (Eq a, Ord b) => <constraints> +This is just an optimisation, but it's why we use topSkolemise to +build the pieces from all the layers, before making a single call +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 always calls checkConstraints, even if there are no skolem + variables at all. Reason: there might be nested deferred errors + that must not be allowed to float to top level. + See Note [When to build an implication] below. +-} + +tcSkolemise, tcSkolemiseScoped + :: UserTypeCtxt -> TcSigmaType + -> (TcType -> TcM result) + -> TcM (HsWrapper, result) + -- ^ The wrapper has type: spec_ty ~> expected_ty + +tcSkolemiseScoped ctxt expected_ty thing_inside + = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty + ; let skol_tvs = map snd tv_prs + skol_info = SigSkol ctxt expected_ty tv_prs + + ; (ev_binds, res) + <- checkConstraints skol_info skol_tvs given $ + tcExtendNameTyVarEnv tv_prs $ + thing_inside rho_ty + + ; return (wrap <.> mkWpLet ev_binds, res) } tcSkolemise ctxt expected_ty thing_inside - -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op - = do { traceTc "tcSkolemise" Outputable.empty - ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty - - ; lvl <- getTcLevel - ; when debugIsOn $ - traceTc "tcSkolemise" $ vcat [ - ppr lvl, - text "expected_ty" <+> ppr expected_ty, - text "inst tyvars" <+> ppr tv_prs, - text "given" <+> ppr given, - text "inst type" <+> ppr rho' ] - - -- Generally we must check that the "forall_tvs" haven't been constrained - -- The interesting bit here is that we must include the free variables - -- of the expected_ty. Here's an example: - -- runST (newVar True) - -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool)) - -- for (newVar True), with s fresh. Then we unify with the runST's arg type - -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool. - -- So now s' isn't unconstrained because it's linked to a. - -- - -- However [Oct 10] now that the untouchables are a range of - -- TcTyVars, all this is handled automatically with no need for - -- extra faffing around + | isRhoTy expected_ty -- Short cut for common case + = do { res <- thing_inside expected_ty + ; return (idHsWrapper, res) } + | otherwise + = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty - ; let tvs' = map snd tv_prs + ; let skol_tvs = map snd tv_prs skol_info = SigSkol ctxt expected_ty tv_prs - ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ - thing_inside tvs' rho' + ; (ev_binds, result) + <- checkConstraints skol_info skol_tvs given $ + thing_inside rho_ty ; return (wrap <.> mkWpLet ev_binds, result) } -- The ev_binds returned by checkConstraints is very @@ -1144,7 +1007,8 @@ tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType tcSkolemiseET _ et@(Infer {}) thing_inside = (idHsWrapper, ) <$> thing_inside et tcSkolemiseET ctxt (Check ty) thing_inside - = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType + = tcSkolemise ctxt ty $ \rho_ty -> + thing_inside (mkCheckExpType rho_ty) checkConstraints :: SkolemInfo -> [TcTyVar] -- Skolems @@ -1162,7 +1026,7 @@ checkConstraints skol_info skol_tvs given thing_inside ; emitImplications implics ; return (ev_binds, result) } - else -- Fast path. We check every function argument with tcCheckExpr, + else -- Fast path. We check every function argument with tcCheckPolyExpr, -- which uses tcSkolemise and hence checkConstraints. -- So this fast path is well-exercised do { res <- thing_inside @@ -1175,38 +1039,33 @@ checkTvConstraints :: SkolemInfo checkTvConstraints skol_info skol_tvs thing_inside = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside - ; emitResidualTvConstraint skol_info Nothing skol_tvs tclvl wanted + ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted ; return result } -emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar] +emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM () -emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted +emitResidualTvConstraint skol_info skol_tvs tclvl wanted | isEmptyWC wanted - , isNothing m_telescope || skol_tvs `lengthAtMost` 1 - -- If m_telescope is (Just d), we must do the bad-telescope check, - -- so we must /not/ discard the implication even if there are no - -- wanted constraints. See Note [Checking telescopes] in GHC.Tc.Types.Constraint. - -- Lacking this check led to #16247 = return () | otherwise - = do { ev_binds <- newNoTcEvBinds + = do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted + ; emitImplication implic } + +buildTvImplication :: SkolemInfo -> [TcTyVar] + -> TcLevel -> WantedConstraints -> TcM Implication +buildTvImplication skol_info skol_tvs tclvl wanted + = do { ev_binds <- newNoTcEvBinds -- Used for equalities only, so all the constraints + -- are solved by filling in coercion holes, not + -- by creating a value-level evidence binding ; implic <- newImplication - ; let status | insolubleWC wanted = IC_Insoluble - | otherwise = IC_Unsolved - -- If the inner constraints are insoluble, - -- we should mark the outer one similarly, - -- so that insolubleWC works on the outer one - - ; emitImplication $ - implic { ic_status = status - , ic_tclvl = tclvl - , ic_skols = skol_tvs - , ic_no_eqs = True - , ic_telescope = m_telescope - , ic_wanted = wanted - , ic_binds = ev_binds - , ic_info = skol_info } } + + ; return (implic { ic_tclvl = tclvl + , ic_skols = skol_tvs + , ic_no_eqs = True + , ic_wanted = wanted + , ic_binds = ev_binds + , ic_info = skol_info }) } implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool -- See Note [When to build an implication] @@ -1319,21 +1178,35 @@ unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' -> TcTauType -> TcTauType -> TcM TcCoercionN -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 -unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType TypeLevel origin ty1 ty2 +unifyType thing ty1 ty2 + = uType TypeLevel origin ty1 ty2 where - origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = ppr <$> thing - , uo_visible = True } -- always called from a visible context + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = ppr <$> thing + , uo_visible = True } + +unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN +-- Like unifyType, but swap expected and actual in error messages +-- This is used when typechecking patterns +unifyTypeET ty1 ty2 + = uType TypeLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped + , uo_expected = ty1 -- NB swapped + , uo_thing = Nothing + , uo_visible = True } + unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN -unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType KindLevel origin ty1 ty2 - where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = ppr <$> thing - , uo_visible = True } -- also always from a visible context +unifyKind thing ty1 ty2 + = uType KindLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = ppr <$> thing + , uo_visible = True } ---------------- {- %************************************************************************ @@ -1639,7 +1512,7 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2 go tv2 | tv1 == tv2 -- Same type variable => no-op = return (mkNomReflCo (mkTyVarTy tv1)) - | swapOverTyVars tv1 tv2 -- Distinct type variables + | swapOverTyVars False tv1 tv2 -- Distinct type variables -- Swap meta tyvar to the left if poss = do { tv1 <- zonkTyCoVarKind tv1 -- We must zonk tv1's kind because that might @@ -1696,8 +1569,12 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 -swapOverTyVars :: TcTyVar -> TcTyVar -> Bool -swapOverTyVars tv1 tv2 +swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool +swapOverTyVars is_given tv1 tv2 + -- See Note [Unification variables on the left] + | not is_given, pri1 == 0, pri2 > 0 = True + | not is_given, pri2 == 0, pri1 > 0 = False + -- Level comparison: see Note [TyVar/TyVar orientation] | lvl1 `strictlyDeeperThan` lvl2 = False | lvl2 `strictlyDeeperThan` lvl1 = True @@ -1786,6 +1663,24 @@ So we look for a positive reason to swap, using a three-step test: Uniques. See Note [Eliminate younger unification variables] (which also explains why we don't do this any more) +Note [Unification variables on the left] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For wanteds, but not givens, swap (skolem ~ meta-tv) regardless of +level, so that the unification variable is on the left. + +* We /don't/ want this for Givens because if we ave + [G] a[2] ~ alpha[1] + [W] Bool ~ a[2] + we want to rewrite the wanted to Bool ~ alpha[1], + so we can float the constraint and solve it. + +* But for Wanteds putting the unification variable on + the left means an easier job when floating, and when + reporting errors -- just fewer cases to consider. + + In particular, we get better skolem-escape messages: + see #18114 + Note [Deeper level on the left] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The most important thing is that we want to put tyvars with diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 4f6b4f5887..32dfc16ea3 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -27,7 +27,7 @@ import GHC.Prelude import GHC.Data.Maybe -- friends: -import GHC.Tc.Utils.Unify ( tcSubType_NC ) +import GHC.Tc.Utils.Unify ( tcSubTypeSigma ) import GHC.Tc.Solver ( simplifyAmbiguityCheck ) import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) ) import GHC.Core.TyCo.FVs @@ -216,7 +216,7 @@ checkAmbiguity ctxt ty ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $ captureConstraints $ - tcSubType_NC ctxt ty ty + tcSubTypeSigma ctxt ty ty ; simplifyAmbiguityCheck ty wanted ; traceTc "Done ambiguity check for" (ppr ty) } diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs index 8cd9a06a06..b08001c6e2 100644 --- a/compiler/GHC/Types/Var.hs +++ b/compiler/GHC/Types/Var.hs @@ -541,11 +541,12 @@ is all about surface syntax. Therefore, they are kept as separate data types. -- Variable Binder -- -- VarBndr is polymorphic in both var and visibility fields. --- Currently there are six different uses of 'VarBndr': --- * Var.TyVarBinder = VarBndr TyVar ArgFlag --- * Var.TyCoVarBinder = VarBndr TyCoVar ArgFlag --- * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis --- * TyCon.TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis +-- Currently there are sevenv different uses of 'VarBndr': +-- * Var.TyVarBinder = VarBndr TyVar ArgFlag +-- * Var.InvisTVBinder = VarBndr TyVar Specificity +-- * Var.TyCoVarBinder = VarBndr TyCoVar ArgFlag +-- * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis +-- * TyCon.TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis -- * IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ArgFlag -- * IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis data VarBndr var argf = Bndr var argf @@ -559,8 +560,8 @@ data VarBndr var argf = Bndr var argf -- -- A 'TyVarBinder' is a binder with only TyVar type TyCoVarBinder = VarBndr TyCoVar ArgFlag -type TyVarBinder = VarBndr TyVar ArgFlag -type InvisTVBinder = VarBndr TyVar Specificity +type TyVarBinder = VarBndr TyVar ArgFlag +type InvisTVBinder = VarBndr TyVar Specificity tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ArgFlag] tyVarSpecToBinders = map tyVarSpecToBinder |