[Git][ghc/ghc][wip/T18412] Allow multiple case branches to have a higher rank type
Simon Peyton Jones
gitlab at gitlab.haskell.org
Fri Jul 10 21:51:48 UTC 2020
Simon Peyton Jones pushed to branch wip/T18412 at Glasgow Haskell Compiler / GHC
Commits:
3ecd7b82 by Simon Peyton Jones at 2020-07-10T22:50:23+01:00
Allow multiple case branches to have a higher rank type
As #18412 points out, it should be OK for multiple case alternatives
to have a higher rank type, provided they are all the same.
This patch implements that change. It sweeps away
GHC.Tc.Gen.Match.tauifyMultipleBranches, and friends, replacing it
with an enhanced version of fillInferResult.
The basic change to fillInferResult is to permit the case in which
another case alternative has already filled in the result; and in
that case simply unify. It's very simple actually.
See the new Note [fillInferResult].
- - - - -
14 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/UsageEnv.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/simplCore/should_compile/T17901.stdout
- + testsuite/tests/typecheck/should_compile/T18412.hs
- testsuite/tests/typecheck/should_compile/all.T
- testsuite/tests/typecheck/should_fail/T10619.stderr
- testsuite/tests/typecheck/should_fail/tcfail002.stderr
- testsuite/tests/typecheck/should_fail/tcfail104.stderr
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -19,7 +19,8 @@ Note [The Type-related module hierarchy]
-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK not-home #-}
-{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-}
+{-# LANGUAGE CPP, MultiWayIf, PatternSynonyms, BangPatterns #-}
+{-# LANGUAGE DeriveDataTypeable #-}
module GHC.Core.TyCo.Rep (
TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing,
@@ -2025,6 +2026,12 @@ GHC.Core.Multiplicity above this module.
-- | A shorthand for data with an attached 'Mult' element (the multiplicity).
data Scaled a = Scaled Mult a
deriving (Data.Data)
+ -- You might think that this would be a natural candiate for
+ -- Functor, Traversable but Krzysztof says (!3674) "it was too easy
+ -- to accidentally lift functions (substitutions, zonking etc.) from
+ -- Type -> Type to Scaled Type -> Scaled Type, ignoring
+ -- multiplicities and causing bugs". So we don't.
+
instance (Outputable a) => Outputable (Scaled a) where
ppr (Scaled _cnt t) = ppr t
=====================================
compiler/GHC/Core/UsageEnv.hs
=====================================
@@ -1,7 +1,7 @@
{-# LANGUAGE ViewPatterns #-}
module GHC.Core.UsageEnv (UsageEnv, addUsage, scaleUsage, zeroUE,
lookupUE, scaleUE, deleteUE, addUE, Usage(..), unitUE,
- supUE, supUEs) where
+ bottomUE, supUE, supUEs) where
import Data.Foldable
import GHC.Prelude
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -591,10 +591,6 @@ tcExpr (HsCase x scrut matches) res_ty
tcExpr (HsIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if'
= do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
- ; res_ty <- tauifyExpType res_ty
- -- Just like Note [Case branches must never infer a non-tau type]
- -- in GHC.Tc.Gen.Match (See #10619)
-
; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty
; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty
; tcEmitBindingUsage (supUE u1 u2)
@@ -611,13 +607,7 @@ tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty
; return (HsIf x fun' pred' b1' b2') }
tcExpr (HsMultiIf _ alts) res_ty
- = do { res_ty <- if isSingleton alts
- then return res_ty
- else tauifyExpType res_ty
- -- Just like GHC.Tc.Gen.Match
- -- Note [Case branches must never infer a non-tau type]
-
- ; alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
+ = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
; res_ty <- readExpType res_ty
; return (HsMultiIf res_ty alts') }
where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -164,80 +164,47 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (mkCheckExpType res_ty)
match_ctxt = MC { mc_what = PatBindRhs,
mc_body = tcBody }
-{-
-************************************************************************
+{- *********************************************************************
* *
-\subsection{tcMatch}
+ tcMatch
* *
-************************************************************************
-
-Note [Case branches must never infer a non-tau type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
- case ... of
- ... -> \(x :: forall a. a -> a) -> x
- ... -> \y -> y
-
-Should that type-check? The problem is that, if we check the second branch
-first, then we'll get a type (b -> b) for the branches, which won't unify
-with the polytype in the first branch. If we check the first branch first,
-then everything is OK. This order-dependency is terrible. So we want only
-proper tau-types in branches (unless a sigma-type is pushed down).
-This is what expTypeToType ensures: it replaces an Infer with a fresh
-tau-type.
-
-An even trickier case looks like
-
- f x True = x undefined
- f x False = x ()
-
-Here, we see that the arguments must also be non-Infer. Thus, we must
-use expTypeToType on the output of matchExpectedFunTys, not the input.
-
-But we make a special case for a one-branch case. This is so that
-
- f = \(x :: forall a. a -> a) -> x
-
-still gets assigned a polytype.
--}
+********************************************************************* -}
--- | When the MatchGroup has multiple RHSs, convert an Infer ExpType in the
--- expected type into TauTvs.
--- See Note [Case branches must never infer a non-tau type]
-tauifyMultipleMatches :: [LMatch id body]
- -> [Scaled ExpType] -> TcM [Scaled ExpType]
-tauifyMultipleMatches group exp_tys
- | isSingletonMatchGroup group = return exp_tys
- | otherwise = mapM (\(Scaled m t) ->
- fmap (Scaled m) (tauifyExpType t)) exp_tys
- -- NB: In the empty-match case, this ensures we fill in the ExpType
+data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module
+ = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is
+ mc_body :: Located (body GhcRn) -- Type checker for a body of
+ -- an alternative
+ -> ExpRhoType
+ -> TcM (Located (body GhcTc)) }
-- | Type-check a MatchGroup.
tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body
-> [Scaled ExpSigmaType] -- Expected pattern types
- -> ExpRhoType -- Expected result-type of the Match.
+ -> ExpRhoType -- Expected result-type of the Match.
-> MatchGroup GhcRn (Located (body GhcRn))
-> TcM (MatchGroup GhcTc (Located (body GhcTc)))
-data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module
- = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is
- mc_body :: Located (body GhcRn) -- Type checker for a body of
- -- an alternative
- -> ExpRhoType
- -> TcM (Located (body GhcTc)) }
tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
, mg_origin = origin })
- = do { (Scaled _ rhs_ty):pat_tys <- tauifyMultipleMatches matches ((Scaled One rhs_ty):pat_tys) -- return type has implicitly multiplicity 1, it doesn't matter all that much in this case since it isn't used and is eliminated immediately.
- -- See Note [Case branches must never infer a non-tau type]
+ | null matches -- Deal with case e of {}
+ -- Since there are no branches, no one else will fill in rhs_ty
+ -- when in inference mode, so we must do it ourselves,
+ -- here, using expTypeToType
+ = do { tcEmitBindingUsage bottomUE
+ ; pat_tys <- mapM scaledExpTypeToType pat_tys
+ ; rhs_ty <- expTypeToType rhs_ty
+ ; return (MG { mg_alts = L l []
+ , mg_ext = MatchGroupTc pat_tys rhs_ty
+ , mg_origin = origin }) }
- ; umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
+ | otherwise
+ = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
; let (usages,matches') = unzip umatches
; tcEmitBindingUsage $ supUEs usages
- ; pat_tys <- mapM (\(Scaled m t) -> fmap (Scaled m) (readExpType t)) pat_tys
+ ; pat_tys <- mapM readScaledExpType pat_tys
; rhs_ty <- readExpType rhs_ty
- ; return (MG { mg_alts = L l matches'
- , mg_ext = MatchGroupTc pat_tys rhs_ty
+ ; return (MG { mg_alts = L l matches'
+ , mg_ext = MatchGroupTc pat_tys rhs_ty
, mg_origin = origin }) }
-------------
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -629,10 +629,9 @@ There are two bits of rebindable syntax:
lit1_ty and lit2_ty could conceivably be different.
var_ty is the type inferred for x, the variable in the pattern.
-If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
-could conceivably be different specializations. But this is very much
-like the situation in Note [Case branches must be taus] in GHC.Tc.Gen.Match.
-So we tauify the pat_ty before proceeding.
+If the pushed-down pattern type isn't a tau-type, the two pat_ty's
+above could conceivably be different specializations. So we use
+expTypeToType on pat_ty before proceeding.
Note that we need to type-check the literal twice, because it is used
twice, and may be used at different types. The second HsOverLit stored in the
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -474,8 +474,6 @@ newOverloadedLit :: HsOverLit GhcRn
newOverloadedLit
lit@(OverLit { ol_val = val, ol_ext = rebindable }) res_ty
| not rebindable
- -- all built-in overloaded lits are tau-types, so we can just
- -- tauify the ExpType
= do { res_ty <- expTypeToType res_ty
; dflags <- getDynFlags
; let platform = targetPlatform dflags
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -36,9 +36,10 @@ module GHC.Tc.Utils.TcMType (
ExpType(..), ExpSigmaType, ExpRhoType,
mkCheckExpType,
newInferExpType,
- readExpType, readExpType_maybe,
- expTypeToType, checkingExpType_maybe, checkingExpType,
- tauifyExpType, inferResultToType,
+ readExpType, readExpType_maybe, readScaledExpType,
+ expTypeToType, scaledExpTypeToType,
+ checkingExpType_maybe, checkingExpType,
+ inferResultToType,
--------------------------------
-- Creating new evidence variables
@@ -396,7 +397,6 @@ checkCoercionHole cv co
Note [ExpType]
~~~~~~~~~~~~~~
-
An ExpType is used as the "expected type" when type-checking an expression.
An ExpType can hold a "hole" that can be filled in by the type-checker.
This allows us to have one tcExpr that works in both checking mode and
@@ -426,14 +426,13 @@ Consider
This is a classic untouchable-variable / ambiguous GADT return type
scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
-And, because there is only one branch of the case, we won't trigger
-Note [Case branches must never infer a non-tau type] of GHC.Tc.Gen.Match.
We thus must track a TcLevel in an Inferring ExpType. If we try to
-fill the ExpType and find that the TcLevels don't work out, we
-fill the ExpType with a tau-tv at the low TcLevel, hopefully to
-be worked out later by some means. This is triggered in
-test gadt/gadt-escape1.
+fill the ExpType and find that the TcLevels don't work out, we fill
+the ExpType with a tau-tv at the low TcLevel, hopefully to be worked
+out later by some means -- see GHC.Tc.Utils.Unify.fillInferResult,
+and Note [fillInferResult] in that module.
+This behaviour triggered in test gadt/gadt-escape1.
-}
-- actual data definition is in GHC.Tc.Utils.TcType
@@ -453,6 +452,12 @@ readExpType_maybe :: ExpType -> TcM (Maybe TcType)
readExpType_maybe (Check ty) = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
+-- | Same as readExpType, but for Scaled ExpTypes
+readScaledExpType :: Scaled ExpType -> TcM (Scaled Type)
+readScaledExpType (Scaled m exp_ty)
+ = do { ty <- readExpType exp_ty
+ ; return (Scaled m ty) }
+
-- | Extract a type out of an ExpType. Otherwise, panics.
readExpType :: ExpType -> TcM TcType
readExpType exp_ty
@@ -472,12 +477,10 @@ checkingExpType :: String -> ExpType -> TcType
checkingExpType _ (Check ty) = ty
checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
-tauifyExpType :: ExpType -> TcM ExpType
--- ^ Turn a (Infer hole) type into a (Check alpha),
--- where alpha is a fresh unification variable
-tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty)
-tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
- ; return (Check ty) }
+scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType)
+scaledExpTypeToType (Scaled m exp_ty)
+ = do { ty <- expTypeToType exp_ty
+ ; return (Scaled m ty) }
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
@@ -488,13 +491,17 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res
inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
, ir_ref = ref })
- = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
+ = do { mb_inferred_ty <- readTcRef ref
+ ; case mb_inferred_ty of {
+ Just ty -> return ty ;
+ Nothing ->
+ do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
-- See Note [TcLevel of ExpType]
; writeMutVar ref (Just tau)
; traceTc "Forcing ExpType to be monomorphic:"
(ppr u <+> text ":=" <+> ppr tau)
- ; return tau }
+ ; return tau } } }
{- *********************************************************************
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -793,33 +793,25 @@ instantiateAndFillInferResult orig ty inf_res
; return (mkWpCastN co <.> wrap) }
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
--- If wrap = fillInferResult t1 t2
--- => wrap :: t1 ~> t2
-fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
- , ir_ref = ref })
- = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty
-
- ; traceTc "Filling ExpType" $
- ppr u <+> text ":=" <+> ppr ty_to_fill_with
-
- ; when debugIsOn (check_hole ty_to_fill_with)
-
- ; writeTcRef ref (Just ty_to_fill_with)
-
- ; return ty_co }
- where
- check_hole ty -- Debug check only
- = do { let ty_lvl = tcTypeLevel ty
- ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
- ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
- ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
- ; cts <- readTcRef ref
- ; case cts of
- Just already_there -> pprPanic "writeExpType"
- (vcat [ ppr u
- , ppr ty
- , ppr already_there ])
- Nothing -> return () }
+-- If co = fillInferResult t1 t2
+-- => co :: t1 ~ t2
+-- See Note [fillInferResult]
+fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl
+ , ir_ref = ref })
+ = do { mb_exp_res_ty <- readTcRef ref
+ ; case mb_exp_res_ty of
+ Just exp_res_ty
+ -> do { traceTc "Joining inferred ExpType" $
+ ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty
+ ; ensureMonoType res_lvl act_res_ty
+ ; unifyType Nothing act_res_ty exp_res_ty }
+ Nothing
+ -> do { traceTc "Filling inferred ExpType" $
+ ppr u <+> text ":=" <+> ppr act_res_ty
+ ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty
+ ; writeTcRef ref (Just act_res_ty)
+ ; return prom_co }
+ }
{- Note [Instantiation of InferResult]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -857,6 +849,81 @@ There is one place where we don't want to instantiate eagerly,
namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type
command. See Note [Implementing :type] in GHC.Tc.Module.
+Note [fillInferResult]
+~~~~~~~~~~~~~~~~~~~~~~
+When inferring, we use fillInferResult to "fill in" the hole in InferResult
+ data InferResult = IR { ir_uniq :: Unique
+ , ir_lvl :: TcLevel
+ , ir_ref :: IORef (Maybe TcType) }
+
+There are two things to worry about:
+
+1. What if it is under a GADT or existential pattern match?
+ - GADTs: a unification variable (and Infer's hole is similar) is untouchable
+ - Existentials: be careful about skolem-escape
+
+2. What if it is filled in more than once? E.g. multiple branches of a case
+ case e of
+ T1 -> e1
+ T2 -> e2
+
+Our typing rules are:
+
+* The RHS of a existential or GADT alternative must always be a
+ monotype, regardless of the number of alternatives.
+
+* Multiple non-existential/GADT branches can have (the same)
+ higher rank type (#18412). E.g. this is OK:
+ case e of
+ True -> hr
+ False -> hr
+ where hr:: (forall a. a->a) -> Int
+ c.f. Section 7.1 of "Practical type inference for arbitrary-rank types"
+ We use choice (2) in that Section.
+ (GHC 8.10 and earlier used choice (1).)
+
+ But note that
+ case e of
+ True -> hr
+ False -> \x -> hr x
+ will fail, because we still /infer/ both branches, so the \x will get
+ a (monotype) unification variable, which will fail to unify with
+ (forall a. a->a)
+
+For (1) we can detect the GADT/existential situation by seeing that
+the current TcLevel is greater than that stored in ir_lvl of the Infer
+ExpType. We bump the level whenever we go past a GADT/existential match.
+
+Then, before filling the hole use promoteTcType to promote the type
+to the outer ir_lvl. promoteTcType does this
+ - create a fresh unification variable alpha at level ir_lvl
+ - emits an equality alpha[ir_lvl] ~ ty
+ - fills the hole with alpha
+That forces the type to be a monotype (since unification variables can
+only unify with monotypes); and catches skolem-escapes because the
+alpha is untouchable until the equality floats out.
+
+For (2), we simply look to see if the hole is filled already.
+ - if not, we promote (as above) and fill the hole
+ - if it is filled, we simply unify with the type that is
+ already there
+
+There is one wrinkle. Suppose we have
+ case e of
+ T1 -> e1 :: (forall a. a->a) -> Int
+ G2 -> e2
+where T1 is not GADT or existential, but G2 is a GADT. Then supppose the
+T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine.
+But now the G2 alternative must not *just* unify with that else we'd risk
+allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first
+we'd have filled the hole with a unification variable, which enforces a
+monotype.
+
+So if we check G2 second, we still want to emit a constraint that restricts
+the RHS to be a monotype. This is done by ensureMonoType, and it works
+by simply generating a constraint (alpha ~ ty), where alpha is a fresh
+unification variable. We discard the evidence.
+
-}
{- *********************************************************************
@@ -865,8 +932,22 @@ command. See Note [Implementing :type] in GHC.Tc.Module.
* *
********************************************************************* -}
+ensureMonoType :: TcLevel -> TcType -> TcM ()
+ensureMonoType dest_lvl res_ty
+ = do { cur_lvl <- getTcLevel
+ ; unless (cur_lvl `sameDepthAs` dest_lvl) $
+ do { mono_ty <- newOpenFlexiTyVarTy
+ ; let eq_orig = TypeEqOrigin { uo_actual = res_ty
+ , uo_expected = mono_ty
+ , uo_thing = Nothing
+ , uo_visible = False }
+
+ ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
+ ; return () } }
+
promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
-- See Note [Promoting a type]
+-- See also Note [fillInferResult]
-- promoteTcType level ty = (co, ty')
-- * Returns ty' whose max level is just 'level'
-- and whose kind is ~# to the kind of 'ty'
=====================================
testsuite/tests/simplCore/should_compile/T17901.stdout
=====================================
@@ -1,14 +1,14 @@
- (wombat1 [Occ=Once*!] :: T -> p)
+ (wombat1 [Occ=Once*!] :: T -> t)
A -> wombat1 T17901.A;
B -> wombat1 T17901.B;
C -> wombat1 T17901.C
- = \ (@p) (wombat1 :: T -> p) (x :: T) ->
+ = \ (@t) (wombat1 :: T -> t) (x :: T) ->
case x of wild { __DEFAULT -> wombat1 wild }
- Tmpl= \ (@p) (wombat2 [Occ=Once!] :: S -> p) (x [Occ=Once] :: S) ->
+ Tmpl= \ (@t) (wombat2 [Occ=Once!] :: S -> t) (x [Occ=Once] :: S) ->
case x of wild [Occ=Once] { __DEFAULT -> wombat2 wild }}]
- = \ (@p) (wombat2 :: S -> p) (x :: S) ->
+ = \ (@t) (wombat2 :: S -> t) (x :: S) ->
case x of wild { __DEFAULT -> wombat2 wild }
- Tmpl= \ (@p) (wombat3 [Occ=Once!] :: W -> p) (x [Occ=Once] :: W) ->
+ Tmpl= \ (@t) (wombat3 [Occ=Once!] :: W -> t) (x [Occ=Once] :: W) ->
case x of wild [Occ=Once] { __DEFAULT -> wombat3 wild }}]
- = \ (@p) (wombat3 :: W -> p) (x :: W) ->
+ = \ (@t) (wombat3 :: W -> t) (x :: W) ->
case x of wild { __DEFAULT -> wombat3 wild }
=====================================
testsuite/tests/typecheck/should_compile/T18412.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T18412 where
+
+hr :: (forall a. a -> a) -> ()
+hr _ = ()
+
+foo x = case x of () -> hr
+
+-- This did not use to be allowed, because the
+-- multiple branches have (the same) polytypes
+-- Enhancement July 2020
+bar x = case x of True -> hr
+ False -> hr
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -716,3 +716,4 @@ test('T17775-viewpats-a', normal, compile, [''])
test('T17775-viewpats-b', normal, compile_fail, [''])
test('T17775-viewpats-c', normal, compile_fail, [''])
test('T17775-viewpats-d', normal, compile_fail, [''])
+test('T18412', normal, compile, [''])
=====================================
testsuite/tests/typecheck/should_fail/T10619.stderr
=====================================
@@ -1,13 +1,11 @@
-T10619.hs:9:15: error:
- • Couldn't match type ‘p’ with ‘forall b. b -> b’
- Expected: p -> p
- Actual: (forall a. a -> a) -> forall b. b -> b
- ‘p’ is a rigid type variable bound by
- the inferred type of foo :: p1 -> p -> p
- at T10619.hs:(8,1)-(10,20)
- • In the expression:
- (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
+T10619.hs:10:14: error:
+ • Couldn't match type ‘p1’ with ‘forall a. a -> a’
+ Expected: (forall a. a -> a) -> forall b. b -> b
+ Actual: p1 -> p1
+ Cannot instantiate unification variable ‘p1’
+ with a type involving polytypes: forall a. a -> a
+ • In the expression: \ y -> y
In the expression:
if True then
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
@@ -19,15 +17,13 @@ T10619.hs:9:15: error:
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
else
\ y -> y
- • Relevant bindings include
- foo :: p1 -> p -> p (bound at T10619.hs:8:1)
T10619.hs:14:15: error:
• Couldn't match type ‘p’ with ‘forall a. a -> a’
Expected: p -> p
Actual: (forall a. a -> a) -> forall b. b -> b
‘p’ is a rigid type variable bound by
- the inferred type of bar :: p1 -> p -> p
+ the inferred type of bar :: p2 -> p -> p
at T10619.hs:(12,1)-(14,66)
• In the expression:
(\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
@@ -43,21 +39,16 @@ T10619.hs:14:15: error:
else
((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b)
• Relevant bindings include
- bar :: p1 -> p -> p (bound at T10619.hs:12:1)
+ bar :: p2 -> p -> p (bound at T10619.hs:12:1)
-T10619.hs:16:13: error:
- • Couldn't match type ‘p’ with ‘forall b. b -> b’
- Expected: p -> p
- Actual: (forall a. a -> a) -> forall b. b -> b
- ‘p’ is a rigid type variable bound by
- the inferred type of baz :: Bool -> p -> p
- at T10619.hs:(16,1)-(17,19)
- • In the expression:
- (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
- In an equation for ‘baz’:
- baz True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b
- • Relevant bindings include
- baz :: Bool -> p -> p (bound at T10619.hs:16:1)
+T10619.hs:17:13: error:
+ • Couldn't match type ‘p0’ with ‘forall a. a -> a’
+ Expected: (forall a. a -> a) -> forall b. b -> b
+ Actual: p0 -> p0
+ Cannot instantiate unification variable ‘p0’
+ with a type involving polytypes: forall a. a -> a
+ • In the expression: \ y -> y
+ In an equation for ‘baz’: baz False = \ y -> y
T10619.hs:20:14: error:
• Couldn't match type ‘p’ with ‘forall a. a -> a’
=====================================
testsuite/tests/typecheck/should_fail/tcfail002.stderr
=====================================
@@ -1,8 +1,8 @@
tcfail002.hs:4:7: error:
- • Couldn't match expected type ‘p’ with actual type ‘[p]’
+ • Couldn't match expected type ‘a’ with actual type ‘[a]’
• In the expression: z
In an equation for ‘c’: c z = z
• Relevant bindings include
- z :: [p] (bound at tcfail002.hs:4:3)
- c :: [p] -> p (bound at tcfail002.hs:3:1)
+ z :: [a] (bound at tcfail002.hs:4:3)
+ c :: [a] -> a (bound at tcfail002.hs:3:1)
=====================================
testsuite/tests/typecheck/should_fail/tcfail104.stderr
=====================================
@@ -1,19 +1,22 @@
-tcfail104.hs:14:12: error:
+tcfail104.hs:16:12: error:
+ • Couldn't match type: Char -> Char
+ with: forall a. a -> a
+ Expected: (forall a. a -> a) -> Char -> Char
+ Actual: (Char -> Char) -> Char -> Char
+ • In the expression: \ x -> x
+ In the expression:
+ if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+ In the expression:
+ (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
+
+tcfail104.hs:22:12: error:
• Couldn't match type: forall a. a -> a
with: Char -> Char
Expected: (Char -> Char) -> Char -> Char
Actual: (forall a. a -> a) -> Char -> Char
• In the expression: \ (x :: forall a. a -> a) -> x
In the expression:
- if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)
+ if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)
In the expression:
- (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c'
-
-tcfail104.hs:22:15: error:
- • Couldn't match expected type: Char -> Char
- with actual type: forall a. a -> a
- • When checking that the pattern signature: forall a. a -> a
- fits the type of its context: Char -> Char
- In the pattern: x :: forall a. a -> a
- In the expression: \ (x :: forall a. a -> a) -> x
+ (if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)) id 'c'
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3ecd7b82c4ac35723d09b5e0eaf6b62808805b6e
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3ecd7b82c4ac35723d09b5e0eaf6b62808805b6e
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200710/3c2941cf/attachment-0001.html>
More information about the ghc-commits
mailing list