Commit 1d118923 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Simple subsumption

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 submodule.
parent 566cc73f
......@@ -745,8 +745,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
......@@ -1679,11 +1678,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
......
......@@ -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,
......@@ -218,6 +218,7 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
, anyTyCon
, boolTyCon
, charTyCon
, stringTyCon
, doubleTyCon
, floatTyCon
, intTyCon
......@@ -297,11 +298,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
......@@ -503,13 +505,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
......@@ -1398,7 +1401,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
......
......@@ -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
......
......@@ -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
{-
%************************************************************************
%* *
......
......@@ -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
......
......@@ -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) ]
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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)
}}}}
......
......@@ -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 []
......
This diff is collapsed.
......@@ -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
......
......@@ -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
......
This diff is collapsed.
......@@ -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
......
This diff is collapsed.
......@@ -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
......
......@@ -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
......
This diff is collapsed.
This diff is collapsed.
......@@ -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
......@@ -406,16 +406,13 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- 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
-- 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
<- matchActualFunTysRho herald expr_orig (Just (unLoc expr)) 1 expr_ty
-- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty)
-- Check that overall pattern is more polymorphic than arg type
......
......@@ -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) } }
......
......@@ -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
......
......@@ -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,