From 831882f23f5df3415f6c719479a3541d51d03d77 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 31 Aug 2016 09:28:39 +0100 Subject: Refactor typechecking of pattern bindings This patch fixes a regression introduced, post 8.0.1, by this major commit: commit 15b9bf4ba4ab47e6809bf2b3b36ec16e502aea72 Author: Simon Peyton Jones Date: Sat Jun 11 23:49:27 2016 +0100 Improve typechecking of let-bindings This major commit was initially triggered by #11339, but it spiraled into a major review of the way in which type signatures for bindings are handled, especially partial type signatures. I didn't get the typechecking of pattern bindings right, leading to Trac #12427. In fixing this I found that this program doesn't work: data T where T :: a -> ((forall b. [b]->[b]) -> Int) -> T h1 y = case y of T _ v -> v Works in 7.10, but not in 8.0.1. There's a happy ending. I found a way to fix this, and improve pattern bindings too. Not only does this fix #12427, but it also allows In particular,we now can accept data T where MkT :: a -> Int -> T ... let { MkT _ q = t } in ... Previously this elicited "my head exploded" but it's really fine since q::Int. The approach is described in detail in TcBinds Note [Typechecking pattern bindings] Super cool. And not even a big patch! --- compiler/typecheck/TcBinds.hs | 226 +++++++++++++-------- compiler/typecheck/TcPat.hs | 187 +++++++++-------- .../tests/typecheck/should_compile/T12427a.hs | 40 ++++ .../tests/typecheck/should_compile/T12427b.hs | 20 ++ testsuite/tests/typecheck/should_compile/all.T | 3 + 5 files changed, 299 insertions(+), 177 deletions(-) create mode 100644 testsuite/tests/typecheck/should_compile/T12427a.hs create mode 100644 testsuite/tests/typecheck/should_compile/T12427b.hs diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 9191667ee9..f2717fcf94 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -1284,69 +1284,81 @@ data TcMonoBind -- Half completed; LHS done, RHS not done | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind +-- Only called with plan InferGen (LetBndrSpec = LetLclBndr) +-- or NoGen (LetBndrSpec = LetGblBndr) +-- CheckGen is used only for functions with a complete type signature, +-- and tcPolyCheck doesn't use tcMonoBinds at all + tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches }) - = do { mono_info <- tcLhsId sig_fn no_gen name + | Just (TcIdSig sig) <- sig_fn name + = -- There is a type signature. + -- It must be partial; if complete we'd be in tcPolyCheck! + -- e.g. f :: _ -> _ + -- f x = ...g... + -- Just g = ...f... + -- Hence always typechecked with InferGen + do { mono_info <- tcLhsSigId no_gen (name, sig) + ; return (TcFunBind mono_info nm_loc matches) } + + | otherwise -- No type signature + = do { mono_ty <- newOpenFlexiTyVarTy + ; mono_id <- newLetBndr no_gen name mono_ty + ; let mono_info = MBI { mbi_poly_name = name + , mbi_sig = Nothing + , mbi_mono_id = mono_id } ; return (TcFunBind mono_info nm_loc matches) } tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) - = do { let bndr_names = collectPatBinders pat - ; mbis <- mapM (tcLhsId sig_fn no_gen) bndr_names - -- See Note [Existentials in pattern bindings] + = -- See Note [Typechecking pattern bindings] + do { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $ - bndr_names `zip` map mbi_mono_id mbis + [ (mbi_poly_name mbi, mbi_mono_id mbi) + | mbi <- sig_mbis ] + + -- See Note [Existentials in pattern bindings] + ; ((pat', nosig_mbis), pat_ty) + <- addErrCtxt (patMonoBindsCtxt pat grhss) $ + tcInferInst $ \ exp_ty -> + tcLetPat inst_sig_fun no_gen pat exp_ty $ + mapM lookup_info nosig_names + + ; let mbis = sig_mbis ++ nosig_mbis ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id) | mbi <- mbis, let id = mbi_mono_id mbi ] $$ ppr no_gen) - ; ((pat', _), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ - tcInferNoInst $ \ exp_ty -> - tcLetPat inst_sig_fun pat exp_ty $ - return () -- mapM (lookup_info inst_sig_fun) bndr_names - ; return (TcPatBind mbis pat' grhss pat_ty) } + where + bndr_names = collectPatBinders pat + (nosig_names, sig_names) = partitionWith find_sig bndr_names + + find_sig :: Name -> Either Name (Name, TcIdSigInfo) + find_sig name = case sig_fn name of + Just (TcIdSig sig) -> Right (name, sig) + _ -> Left name + + -- After typechecking the pattern, look up the binder + -- names that lack a signature, which the pattern has brought + -- into scope. + lookup_info :: Name -> TcM MonoBindInfo + lookup_info name + = do { mono_id <- tcLookupId name + ; return (MBI { mbi_poly_name = name + , mbi_sig = Nothing + , mbi_mono_id = mono_id }) } tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind) -- AbsBind, VarBind impossible ------------------- -data LetBndrSpec - = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds - -- so clone a fresh binder for the local monomorphic Id - - | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going - -- to be an AbsBinds; So we must bind the global version - -- of the binder right away. - -- And here is the inline-pragma information - -instance Outputable LetBndrSpec where - ppr LetLclBndr = text "LetLclBndr" - ppr (LetGblBndr {}) = text "LetGblBndr" - -tcLhsId :: TcSigFun -> LetBndrSpec -> Name -> TcM MonoBindInfo -tcLhsId sig_fn no_gen name - | Just (TcIdSig sig) <- sig_fn name - = -- A partial type signature on a FunBind, in a mixed group - -- e.g. f :: _ -> _ - -- f x = ...g... - -- Just g = ...f... - -- Hence always typechecked with InferGen; hence LetLclBndr - -- - -- A compelete type sig on a FunBind is checked with CheckGen - -- and does not go via tcLhsId - do { inst_sig <- tcInstSig sig - ; the_id <- newSigLetBndr no_gen name inst_sig +tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo +tcLhsSigId no_gen (name, sig) + = do { inst_sig <- tcInstSig sig + ; mono_id <- newSigLetBndr no_gen name inst_sig ; return (MBI { mbi_poly_name = name , mbi_sig = Just inst_sig - , mbi_mono_id = the_id }) } - - | otherwise - = -- No type signature, plan InferGen (LetLclBndr) or NoGen (LetGblBndr) - do { mono_ty <- newOpenFlexiTyVarTy - ; mono_id <- newLetBndr no_gen name mono_ty - ; return (MBI { mbi_poly_name = name - , mbi_sig = Nothing , mbi_mono_id = mono_id }) } ------------ @@ -1357,20 +1369,6 @@ newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig }) newSigLetBndr no_gen name (TISI { sig_inst_tau = tau }) = newLetBndr no_gen name tau -newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId --- In the polymorphic case when we are going to generalise --- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version" --- of the Id; the original name will be bound to the polymorphic version --- by the AbsBinds --- In the monomorphic case when we are not going to generalise --- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds, --- and we use the original name directly -newLetBndr LetLclBndr name ty - = do { mono_name <- cloneLocalName name - ; return (mkLocalId mono_name ty) } -newLetBndr (LetGblBndr prags) name ty - = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name) - ------------------- tcRhs :: TcMonoBind -> TcM (HsBind TcId) tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id }) @@ -1439,9 +1437,13 @@ getMonoBindInfo tc_binds get_info (TcFunBind info _ _) rest = info : rest get_info (TcPatBind infos _ _ _) rest = infos ++ rest -{- Note [Existentials in pattern bindings] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider (typecheck/should_compile/ExPat): + +{- Note [Typechecking pattern bindings] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Look at: + - typecheck/should_compile/ExPat + - Trac #12427, typecheck/should_compile/T12427{a,b} + data T where MkT :: Integral a => a -> Int -> T @@ -1453,48 +1455,96 @@ and suppose t :: T. Which of these pattern bindings are ok? E3. let { MkT (toInteger -> r) _ = t } in -Well (E1) is clearly wrong because the existential 'a' escapes. -What type could 'p' possibly have? +* (E1) is clearly wrong because the existential 'a' escapes. + What type could 'p' possibly have? -But (E2) is fine, despite the existential pattern, because -q::Int, and nothing escapes. +* (E2) is fine, despite the existential pattern, because + q::Int, and nothing escapes. -Even (E3) is fine. The existential pattern binds a dictionary -for (Integral a) which the view pattern can use to convert the -a-valued field to an Integer, so r :: Integer. +* Even (E3) is fine. The existential pattern binds a dictionary + for (Integral a) which the view pattern can use to convert the + a-valued field to an Integer, so r :: Integer. An easy way to see all three is to imagine the desugaring. -For (2) it would look like +For (E2) it would look like let q = case t of MkT _ q' -> q' in -We typecheck pattern bindings as follows: - 1. In tcLhs we bind q'::alpha, for each variable q bound by the - pattern, where q' is a fresh name, and alpha is a fresh - unification variable; it will be the monomorphic verion of q that - we later generalise - It's very important that these fresh unification variables - alpha are born here, not deep under implications as would happen - if we allocated them when we encountered q during tcPat. +We typecheck pattern bindings as follows. First tcLhs does this: + + 1. Take each type signature q :: ty, partial or complete, and + instantiate it (with tcLhsSigId) to get a MonoBindInfo. This + gives us a fresh "mono_id" qm :: instantiate(ty), where qm has + a fresh name. + + Any fresh unification variables in instiatiate(ty) born here, not + deep under implications as would happen if we allocated them when + we encountered q during tcPat. - 2. Still in tcLhs, we build a little environment mappting "q" -> - q':alpha, and pass that to tcLetPet. + 2. Build a little environment mapping "q" -> "qm" for those Ids + with signatures (inst_sig_fun) - 3. Then tcLhs invokes tcLetPat to typecheck the patter as usual: - - When tcLetPat finds an existential constructor, it binds fresh - type variables and dictionaries as usual, and emits an - implication constraint. + 3. Invoke tcLetPat to typecheck the pattern. - - When tcLetPat finds a variable (TcPat.tcPatBndr) it looks it up - in the little environment, which should always succeed. And - uses tcSubTypeET to connect the type of that variable with the - expected type of the pattern. + - We pass in the current TcLevel. This is captured by + TcPat.tcLetPat, and put into the pc_lvl field of PatCtxt, in + PatEnv. + - When tcPat finds an existential constructor, it binds fresh + type variables and dictionaries as usual, increments the TcLevel, + and emits an implication constraint. + + - When we come to a binder (TcPat.tcPatBndr), it looks it up + in the little environment (the pc_sig_fn field of PatCtxt). + + Success => There was a type signature, so just use it, + checking compatibility with the expected type. + + Failure => No type sigature. + Infer case: (happens only outside any constructor pattern) + use a unification variable + at the outer level pc_lvl + + Check case: use promoteTcType to promote the type + to the outer level pc_lvl. This is the + place where we emit a constraint that'll blow + up if existential capture takes place + + Result: the type of the binder is always at pc_lvl. This is + crucial. + + 4. Throughout, when we are making up an Id for the pattern-bound variables + (newLetBndr), we have two cases: + + - If we are generalising (generalisation plan is InferGen or + CheckGen), then the let_bndr_spec will be LetLclBndr. In that case + we want to bind a cloned, local version of the variable, with the + type given by the pattern context, *not* by the signature (even if + there is one; see Trac #7268). The mkExport part of the + generalisation step will do the checking and impedance matching + against the signature. + + - If for some some reason we are not generalising (plan = NoGen), the + LetBndrSpec will be LetGblBndr. In that case we must bind the + global version of the Id, and do so with precisely the type given + in the signature. (Then we unify with the type from the pattern + context type.) + + And that's it! The implication constraints check for the skolem -escape. It's quite simple and neat, and more exressive than before +escape. It's quite simple and neat, and more expressive than before e.g. GHC 8.0 rejects (E2) and (E3). +Example for (E1), starting at level 1. We generate + p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta) +The (a~beta) can't float (because of the 'a'), nor be solved (because +beta is untouchable.) + +Example for (E2), we generate + q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta) +The beta is untoucable, but floats out of the constraint and can +be solved absolutely fine. ************************************************************************ * * diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index 7900d6c592..5a1cbfadc6 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -9,7 +9,7 @@ TcPat: Typechecking patterns {-# LANGUAGE CPP, RankNTypes, TupleSections #-} {-# LANGUAGE FlexibleContexts #-} -module TcPat ( tcLetPat +module TcPat ( tcLetPat, newLetBndr, LetBndrSpec(..) , tcPat, tcPat_O, tcPats , addDataConStupidTheta, badFieldCon, polyPatSig ) where @@ -19,6 +19,7 @@ import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma ) import HsSyn import TcHsSyn +import TcSigs( TcPragEnv, lookupPragEnv, addInlinePrags ) import TcRnMonad import Inst import Id @@ -58,15 +59,20 @@ import ListSetOps ( getNth ) -} tcLetPat :: (Name -> Maybe TcId) + -> LetBndrSpec -> LPat Name -> ExpSigmaType -> TcM a -> TcM (LPat TcId, a) -tcLetPat sig_fn pat pat_ty thing_inside - = tc_lpat pat pat_ty penv thing_inside - where - penv = PE { pe_lazy = True - , pe_ctxt = LetPat sig_fn - , pe_orig = PatOrigin } +tcLetPat sig_fn no_gen pat pat_ty thing_inside + = do { bind_lvl <- getTcLevel + ; let ctxt = LetPat { pc_lvl = bind_lvl + , pc_sig_fn = sig_fn + , pc_new = no_gen } + penv = PE { pe_lazy = True + , pe_ctxt = ctxt + , pe_orig = PatOrigin } + + ; tc_lpat pat pat_ty penv thing_inside } ----------------- tcPats :: HsMatchContext Name @@ -109,7 +115,14 @@ tcPat_O ctxt orig pat pat_ty thing_inside penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig } ------------------ +{- +************************************************************************ +* * + PatEnv, PatCtxt, LetBndrSpec +* * +************************************************************************ +-} + data PatEnv = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears @@ -122,7 +135,29 @@ data PatCtxt | LetPat -- Used only for let(rec) pattern bindings -- See Note [Typing patterns in pattern bindings] - (Name -> Maybe TcId) -- Tells the expected type for this binder + { pc_lvl :: TcLevel + -- Level of the binding group + + , pc_sig_fn :: Name -> Maybe TcId + -- Tells the expected type + -- for binders with a signature + + , pc_new :: LetBndrSpec + -- How to make a new binder + } -- for binders without signatures + +data LetBndrSpec + = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds + -- so clone a fresh binder for the local monomorphic Id + + | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going + -- to be an AbsBinds; So we must bind the global version + -- of the binder right away. + -- And here is the inline-pragma information + +instance Outputable LetBndrSpec where + ppr LetLclBndr = text "LetLclBndr" + ppr (LetGblBndr {}) = text "LetGblBndr" makeLazy :: PatEnv -> PatEnv makeLazy penv = penv { pe_lazy = True } @@ -141,101 +176,75 @@ tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId) -- (coi, xp) = tcPatBndr penv x pat_ty -- Then coi : pat_ty ~ typeof(xp) -- -tcPatBndr penv@(PE { pe_ctxt = LetPat lookup_sig - , pe_orig = orig }) - bndr_name pat_ty - -- See Note [Typing patterns in pattern bindings] - | Just bndr_id <- lookup_sig bndr_name - = do { wrap <- tcSubTypePat penv orig pat_ty (idType bndr_id) - ; traceTc "tcPatBndr(lsl,sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr pat_ty) +tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl + , pc_sig_fn = sig_fn + , pc_new = no_gen } }) + bndr_name exp_pat_ty + -- For the LetPat cases, see + -- Note [Typechecking pattern bindings] in TcBinds + + | Just bndr_id <- sig_fn bndr_name -- There is a signature + = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id) + -- See Note [Subsumption check at pattern variables] + ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty) ; return (wrap, bndr_id) } - | otherwise -- No signature - = pprPanic "tcPatBndr" (ppr bndr_name) - -tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty + | otherwise -- No signature + = do { (co, bndr_ty) <- case exp_pat_ty of + Check pat_ty -> promoteTcType bind_lvl pat_ty + Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res ) + -- If we were under a constructor that bumped + -- the level, we'd be in checking mode + do { bndr_ty <- inferResultToType infer_res + ; return (mkTcNomReflCo bndr_ty, bndr_ty) } + ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty + ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl + , ppr exp_pat_ty, ppr bndr_ty, ppr co + , ppr bndr_id ]) + ; return (mkWpCastN co, bndr_id) } + +tcPatBndr _ bndr_name pat_ty = do { pat_ty <- expTypeToType pat_ty ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty) ; return (idHsWrapper, mkLocalId bndr_name pat_ty) } -- Whether or not there is a sig is irrelevant, -- as this is local +newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId +-- Make up a suitable Id for the pattern-binder. +-- See Note [Typechecking pattern bindings], item (4) in TcBinds +-- +-- In the polymorphic case when we are going to generalise +-- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version" +-- of the Id; the original name will be bound to the polymorphic version +-- by the AbsBinds +-- In the monomorphic case when we are not going to generalise +-- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds, +-- and we use the original name directly +newLetBndr LetLclBndr name ty + = do { mono_name <- cloneLocalName name + ; return (mkLocalId mono_name ty) } +newLetBndr (LetGblBndr prags) name ty + = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name) + tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt -- Used when typechecking patterns tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2 -{- Note [Partial signatures for pattern bindings] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider a function binding and a pattern binding, both -with a partial type signature - - f1 :: (True, _) -> Char - f1 = \x -> x - - f2 :: (True, _) -> Char - Just f2 = Just (\x->x) +{- Note [Subsumption check at pattern variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we come across a variable with a type signature, we need to do a +subsumption, not equality, check against the context type. e.g. -Obviously, both should be rejected. That happens naturally for the -function binding, f1, because we typecheck the RHS with "expected" -type '(True, apha) -> Char', which correctly fails. - -But what of the pattern binding for f2? We infer the type of the -pattern, and check tha the RHS has that type. So we must feed in the -type of f2 when inferring the type of the pattern! We do this right -here, in tcPatBndr, for a LetLclBndr. The signature already has fresh -unification variables for the wildcards (if any). - -Extra notes - -* For /complete/ type signatures, we could im principle ignore all this - and just infer the most general type for f2, and check (in - TcBinds.mkExport) whether it has the claimed type. - - But not so for /partial/ signatures; to get the wildcard unification - variables into the game we really must inject them here. If we don't - we never get /any/ value assigned to the wildcards; and programs that - are bogus, like f2, are accepted. - - Moreover, by feeding in the expected type we do less fruitless - creation of unification variables, and improve error messages. - -* We need to do a subsumption, not equality, check. If - data T = MkT (forall a. a->a) + data T = MkT (forall a. a->a) f :: forall b. [b]->[b] MkT f = blah - Since 'blah' returns a value of type T, its payload is a polymorphic - function of type (forall a. a->a). And that's enough to bind the - less-polymorphic function 'f', but we need some impedence matching - to witness the instantiation. - -Note [Typing patterns in pattern bindings] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we are typing a pattern binding - pat = rhs -Then the PatCtxt will be (LetPat sig_fn). - -There can still be signatures for the binders: - data T = MkT (forall a. a->a) Int - x :: forall a. a->a - y :: Int - MkT x y = - -Two cases, dealt with by the LetPat case of tcPatBndr - - * If we are generalising (generalisation plan is InferGen or - CheckGen), then the let_bndr_spec will be LetLclBndr. In that case - we want to bind a cloned, local version of the variable, with the - type given by the pattern context, *not* by the signature (even if - there is one; see Trac #7268). The mkExport part of the - generalisation step will do the checking and impedance matching - against the signature. - - * If for some some reason we are not generalising (plan = NoGen), the - LetBndrSpec will be LetGblBndr. In that case we must bind the - global version of the Id, and do so with precisely the type given - in the signature. (Then we unify with the type from the pattern - context type.) + +Since 'blah' returns a value of type T, its payload is a polymorphic +function of type (forall a. a->a). And that's enough to bind the +less-polymorphic function 'f', but we need some impedence matching +to witness the instantiation. ************************************************************************ @@ -1124,7 +1133,7 @@ Lazy patterns can't bind existentials. They arise in two ways: The pe_lazy field of PatEnv says whether we are inside a lazy pattern (perhaps deeply) -See also Note [Existentials in pattern bindings] in TcBinds +See also Note [Typechecking pattern bindings] in TcBinds -} maybeWrapPatCtxt :: Pat Name -> (TcM a -> TcM b) -> TcM a -> TcM b diff --git a/testsuite/tests/typecheck/should_compile/T12427a.hs b/testsuite/tests/typecheck/should_compile/T12427a.hs new file mode 100644 index 0000000000..1cbf7c5c27 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427a.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE GADTs, RankNTypes #-} + +-- Test pattern bindings, existentials, and higher rank + +module T12427a where + +data T where + T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T + T2 :: ((forall b. [b]->[b]) -> Int) -> T + +-- Inference +-- Worked in 7.10 (probably wrongly) +-- Failed in 8.0.1 +-- Fails in 8.2 because v is polymorphic +-- and the T1 pattern match binds existentials, +-- and hence bumps levels +h11 y = case y of T1 _ v -> v + +-- Worked in 7.10 (probably wrongly) +-- Failed in 8.0.1 +-- Succeeds in 8.2 because the pattern match has +-- no existentials, so it doesn't matter than +-- v is polymoprhic +h12 y = case y of T2 v -> v + +-- Inference +-- Same results as for h11 and h12 resp +T1 _ x1 = undefined +T2 x2 = undefined + +-- Works in all versions +h2 :: T -> (forall b. [b] -> [b]) -> Int +h2 y = case y of T1 _ v -> v + +-- Checking +-- Fails in 7.10 (head exploded) +-- Fails in 8.0.1 (ditto) +-- Succeeds in 8.2 +x3 :: (forall a. a->a) -> Int +T1 _ x3 = undefined diff --git a/testsuite/tests/typecheck/should_compile/T12427b.hs b/testsuite/tests/typecheck/should_compile/T12427b.hs new file mode 100644 index 0000000000..11413dc5e5 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427b.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE GADTs, RankNTypes #-} + +module T12427b where + +newtype Acquire a = Acquire {unAcquire :: (forall b. b -> b) -> IO a} + +instance Functor Acquire where + fmap = undefined + +instance Applicative Acquire where + pure = undefined + (<*>) = undefined + +instance Monad Acquire where + Acquire f >>= g' = Acquire $ \restore -> do + x <- f restore + let Acquire g = g' x + -- let g = unAcquire (g' x) + g restore + diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index f107ba16d6..9f32b44d31 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -533,3 +533,6 @@ test('T12185', normal, compile, ['']) test('T12133', normal, compile, ['']) test('T12381', normal, compile, ['']) test('T12082', normal, compile, ['']) +test('T12427a', normal, compile_fail, ['']) +test('T12427b', normal, compile, ['']) + -- cgit v1.2.1