Commit 45bfd1a6 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Refactor typechecking of pattern bindings

This patch fixes a regression introduced, post 8.0.1, by
this major commit:

     commit 15b9bf4b
     Author: Simon Peyton Jones <simonpj@microsoft.com>
     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!
parent ff225b49
......@@ -1262,69 +1262,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) $
tcInfer $ \ 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 }) }
------------
......@@ -1335,20 +1347,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 })
......@@ -1417,9 +1415,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
......@@ -1431,48 +1433,96 @@ and suppose t :: T. Which of these pattern bindings are ok?
E3. let { MkT (toInteger -> r) _ = t } in <body>
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 <body>
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. Build a little environment mapping "q" -> "qm" for those Ids
with signatures (inst_sig_fun)
2. Still in tcLhs, we build a little environment mappting "q" ->
q':alpha, and pass that to tcLetPet.
3. Invoke tcLetPat to typecheck the pattern.
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.
- 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.)
- 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.
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.
************************************************************************
* *
......
......@@ -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,95 +176,75 @@ tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
-- (coi, xp) = tcPatBndr penv x pat_ty
-- Then coi : pat_ty ~ typeof(xp)
--
tcPatBndr (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 <- tcSubTypeET 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
{- 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)
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)
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 [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.
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 = <rhs>
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.
************************************************************************
......@@ -1132,7 +1147,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
......
{-# 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
{-# 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
......@@ -545,3 +545,5 @@ test('T12170b', normal, compile, [''])
test('T12466', normal, compile, [''])
test('T12466a', normal, compile, [''])
test('T12644', normal, compile, [''])
test('T12427a', normal, compile_fail, [''])
test('T12427b', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment