Commit 08ba691a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Take account of kinds in promoteTcType

One of the ASSERT failures in Trac #12762, namely the one for T4439,
showed that I had not dealt correctly with promoting the kind of
a type in promoteTcType.

Happily I could fix this by simplifying InferRes (eliminating the
ir_kind field), so things get better. And the ASSERT is fixed.
parent 1221f810
......@@ -54,7 +54,6 @@ import NameSet
import RdrName
import TyCon
import Type
import TysPrim ( tYPE )
import TcEvidence
import VarSet
import TysWiredIn
......@@ -1743,8 +1742,8 @@ tcSeq loc fun_name args res_ty
; (arg1, arg2, arg2_exp_ty) <- case args1 of
[Right hs_ty_arg2, Left term_arg1, Left term_arg2]
-> do { rr_ty <- newFlexiTyVarTy runtimeRepTy
; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty)
-> do { arg2_kind <- newOpenTypeKind
; ty_arg2 <- tcHsTypeApp hs_ty_arg2 arg2_kind
-- see Note [Typing rule for seq]
; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg2 res_ty
; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) }
......
......@@ -200,8 +200,7 @@ tcHsSigType ctxt sig_ty
do { kind <- case expectedKindInCtxt ctxt of
AnythingKind -> newMetaKindVar
TheKind k -> return k
OpenKind -> do { rr <- newFlexiTyVarTy runtimeRepTy
; return $ tYPE rr }
OpenKind -> newOpenTypeKind
-- The kind is checked by checkValidType, and isn't necessarily
-- of kind * in a Template Haskell quote eg [t| Maybe |]
......@@ -305,7 +304,7 @@ tcHsOpenType, tcHsLiftedType,
tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
tcHsOpenTypeNC ty = do { ek <- ekOpen
tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
; tc_lhs_type typeLevelMode ty ek }
tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
......@@ -464,10 +463,10 @@ tc_lhs_type mode (L span ty) exp_kind
tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
TypeLevel ->
do { arg_rr <- newFlexiTyVarTy runtimeRepTy
; res_rr <- newFlexiTyVarTy runtimeRepTy
; ty1' <- tc_lhs_type mode ty1 (tYPE arg_rr)
; ty2' <- tc_lhs_type mode ty2 (tYPE res_rr)
do { arg_k <- newOpenTypeKind
; res_k <- newOpenTypeKind
; ty1' <- tc_lhs_type mode ty1 arg_k
; ty2' <- tc_lhs_type mode ty2 res_k
; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
KindLevel -> -- no representation polymorphism in kinds. yet.
do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
......@@ -534,8 +533,9 @@ tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind
-- See Note [Body kind of a HsQualTy]
; ty' <- if isConstraintKind exp_kind
then tc_lhs_type mode ty constraintKind
else do { ek <- ekOpen -- The body kind (result of the
-- function) can be * or #, hence ekOpen
else do { ek <- newOpenTypeKind
-- The body kind (result of the function)
-- can be * or #, hence newOpenTypeKind
; ty <- tc_lhs_type mode ty ek
; checkExpectedKind ty liftedTypeKind exp_kind }
......@@ -594,8 +594,8 @@ tc_hs_type mode (HsTupleTy hs_tup_sort tys) exp_kind
tc_hs_type mode (HsSumTy hs_tys) exp_kind
= do { let arity = length hs_tys
; arg_kinds <- map tYPE `fmap` newFlexiTyVarTys arity runtimeRepTy
; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
; let arg_tys = map (getRuntimeRepFromKind "tc_hs_type HsSumTy") arg_kinds ++ tau_tys
; checkExpectedKind (mkTyConApp (sumTyCon arity) arg_tys) (tYPE unboxedSumRepDataConTy) exp_kind
}
......@@ -692,8 +692,7 @@ tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType
tc_tuple mode tup_sort tys exp_kind
= do { arg_kinds <- case tup_sort of
BoxedTuple -> return (nOfThem arity liftedTypeKind)
UnboxedTuple -> do { rrs <- newFlexiTyVarTys arity runtimeRepTy
; return $ map tYPE rrs }
UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
ConstraintTuple -> return (nOfThem arity constraintKind)
; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
; finish_tuple tup_sort tau_tys arg_kinds exp_kind }
......@@ -1989,11 +1988,6 @@ in-scope variables that it should not unify with, but it's fiddly.
-}
-- | Produce an 'TcKind' suitable for a checking a type that can be * or #.
ekOpen :: TcM TcKind
ekOpen = do { rr <- newFlexiTyVarTy runtimeRepTy
; return (tYPE rr) }
unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
unifyKinds act_kinds
= do { kind <- newMetaKindVar
......
......@@ -19,8 +19,8 @@ module TcMType (
newFlexiTyVar,
newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newOpenFlexiTyVarTy,
newMetaKindVar, newMetaKindVars,
newOpenFlexiTyVarTy, newOpenTypeKind,
newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
cloneMetaTyVar,
newFmvTyVar, newFskTyVar,
......@@ -34,7 +34,7 @@ module TcMType (
newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
readExpType, readExpType_maybe,
expTypeToType, checkingExpType_maybe, checkingExpType,
tauifyExpType, inferResultToType, promoteTcType,
tauifyExpType, inferResultToType,
--------------------------------
-- Creating fresh type variables for pm checking
......@@ -345,15 +345,12 @@ newInferExpTypeInst = newInferExpType True
newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
= do { rr <- newFlexiTyVarTy runtimeRepTy
; u <- newUnique
= do { u <- newUnique
; tclvl <- getTcLevel
; let ki = tYPE rr
; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
; ref <- newMutVar Nothing
; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
, ir_kind = ki, ir_ref = ref
, ir_inst = inst })) }
, ir_ref = ref, ir_inst = inst })) }
-- | Extract a type out of an ExpType, if one exists. But one should always
-- exist. Unless you're quite sure you know what you're doing.
......@@ -395,126 +392,21 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res
inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
, ir_kind = kind, ir_ref = ref })
= do { tau_tv <- newMetaTyVarAtLevel tc_lvl kind
, ir_ref = ref })
= do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
-- See Note [TcLevel of ExpType]
; let tau = mkTyVarTy tau_tv
; writeMutVar ref (Just tau)
; traceTc "Forcing ExpType to be monomorphic:"
(ppr u <+> dcolon <+> ppr kind <+> text ":=" <+> ppr tau)
(ppr u <+> text ":=" <+> ppr tau)
; return tau }
{- *********************************************************************
* *
Promoting types
* *
********************************************************************* -}
promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
-- See Note [Promoting a type]
-- promoteTcType level ty = (co, ty')
-- * Returns ty' whose max level is just 'level'
-- and whose kind is the same as 'ty'
-- * and co :: ty ~ ty'
-- * and emits constraints to justify the coercion
promoteTcType dest_lvl ty
= do { cur_lvl <- getTcLevel
; if (cur_lvl `sameDepthAs` dest_lvl)
then dont_promote_it
else promote_it }
where
promote_it :: TcM (TcCoercion, TcType)
promote_it
= do { prom_tv <- newMetaTyVarAtLevel dest_lvl (typeKind ty)
; let prom_ty = mkTyVarTy prom_tv
eq_orig = TypeEqOrigin { uo_actual = ty
, uo_expected = prom_ty
, uo_thing = Nothing }
; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
; return (co, prom_ty) }
dont_promote_it :: TcM (TcCoercion, TcType)
dont_promote_it = return (mkTcNomReflCo ty, ty)
{- Note [Promoting a type]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #12427)
data T where
MkT :: (Int -> Int) -> a -> T
h y = case y of MkT v w -> v
We'll infer the RHS type with an expected type ExpType of
(IR { ir_lvl = l, ir_ref = ref, ... )
where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
match will increase the level, so we'll end up in tcSubType, trying to
unify the type of v,
v :: Int -> Int
with the expected type. But this attempt takes place at level (l+1),
rightly so, since v's type could have mentioned existential variables,
(like w's does) and we want to catch that.
So we
- create a new meta-var alpha[l+1]
- fill in the InferRes ref cell 'ref' with alpha
- emit an equality constraint, thus
[W] alpha[l+1] ~ (Int -> Int)
That constraint will float outwards, as it should, unless v's
type mentions a skolem-captured variable.
This approach fails if v has a higher rank type; see
Note [Promotion and higher rank types]
Note [Promotion and higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
then we'd emit an equality
[W] alpha[l+1] ~ ((forall a. a->a) -> Int)
which will sadly fail because we can't unify a unification variable
with a polytype. But there is nothing really wrong with the program
here.
We could just about solve this by "promote the type" of v, to expose
its polymorphic "shape" while still leaving constraints that will
prevent existential escape. But we must be careful! Exposing
the "shape" of the type is precisely what we must NOT do under
a GADT pattern match! So in this case we might promote the type
to
(forall a. a->a) -> alpha[l+1]
and emit the constraint
[W] alpha[l+1] ~ Int
Now the poromoted type can fill the ref cell, while the emitted
equality can float or not, according to the usual rules.
But that's not quite right! We are exposing the arrow! We could
deal with that too:
(forall a. mu[l+1] a a) -> alpha[l+1]
with constraints
[W] alpha[l+1] ~ Int
[W] mu[l+1] ~ (->)
Here we abstract over the '->' inside the forall, in case that
is subject to an equality constraint from a GADT match.
Note that we kept the outer (->) becuase that's part of
the polymorphic "shape". And becauuse of impredicativity,
GADT matches can't give equalities that affect polymorphic
shape.
This reasoning just seems too complicated, so I decided not
to do it. These higher-rank notes are just here to record
the thinking.
************************************************************************
{- *********************************************************************
* *
SkolemTvs (immutable)
* *
************************************************************************
-}
********************************************************************* -}
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
-- ^ How to instantiate the type variables
......@@ -861,7 +753,7 @@ newAnonMetaTyVar meta_info kind
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy :: Kind -> TcM TcType
newFlexiTyVarTy kind = do
tc_tyvar <- newFlexiTyVar kind
return (mkTyVarTy tc_tyvar)
......@@ -869,11 +761,17 @@ newFlexiTyVarTy kind = do
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
= do { rr <- newFlexiTyVarTy runtimeRepTy
; return (tYPE rr) }
-- | Create a tyvar that can be a lifted or unlifted type.
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
= do { rr <- newFlexiTyVarTy runtimeRepTy
; newFlexiTyVarTy (tYPE rr) }
= do { kind <- newOpenTypeKind
; newFlexiTyVarTy kind }
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
......@@ -913,15 +811,15 @@ new_meta_tv_x info subst tv
subst1 = extendTvSubstWithClone subst tv new_tv
; return (subst1, new_tv) }
newMetaTyVarAtLevel :: TcLevel -> TcKind -> TcM TcTyVar
newMetaTyVarAtLevel tc_lvl kind
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
= do { uniq <- newUnique
; ref <- newMutVar Flexi
; let name = mkMetaTyVarName uniq (fsLit "p")
details = MetaTv { mtv_info = TauTv
, mtv_ref = ref
, mtv_tclvl = tc_lvl }
; return (mkTcTyVar name kind details) }
; return (mkTyVarTy (mkTcTyVar name kind details)) }
{- Note [Name of an instantiated type variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -390,7 +390,7 @@ tcPatSynMatcher (L loc name) lpat
; tv_name <- newNameAt (mkTyVarOcc "r") loc
; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
rr = mkTyVarTy rr_tv
res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
res_ty = mkTyVarTy res_tv
is_unlifted = null args && null prov_dicts
(cont_args, cont_arg_tys)
......
......@@ -305,8 +305,9 @@ data InferResult
-- i.e. return a RhoType
-- False <=> do not instantaite before returning
-- i.e. return a SigmaType
, ir_kind :: Kind
, ir_ref :: IORef (Maybe TcType) }
-- The type that fills in this hole should be a Type,
-- that is, its kind should be (TYPE rr) for some rr
type ExpSigmaType = ExpType
type ExpRhoType = ExpType
......@@ -317,9 +318,8 @@ instance Outputable ExpType where
instance Outputable InferResult where
ppr (IR { ir_uniq = u, ir_lvl = lvl
, ir_kind = ki, ir_inst = inst })
, ir_inst = inst })
= text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
<+> dcolon <+> ppr ki
-- | Make an 'ExpType' suitable for checking.
mkCheckExpType :: TcType -> ExpType
......
......@@ -17,7 +17,7 @@ module TcUnify (
-- Various unifications
unifyType, unifyTheta, unifyKind, noThing,
uType,
uType, promoteTcType,
swapOverTyVars, canSolveByUnification,
--------------------------------
......@@ -52,6 +52,7 @@ import Name ( isSystemName )
import Inst
import TyCon
import TysWiredIn
import TysPrim( tYPE )
import Var
import VarSet
import VarEnv
......@@ -830,34 +831,24 @@ fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me })
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
-- If wrap = fillInferResult t1 t2
-- => wrap :: t1 ~> t2
fillInferResult ty (IR { ir_uniq = u, ir_lvl = res_lvl
, ir_kind = res_kind, ir_ref = ref })
= do { (ty_co, ty) <- promoteTcType res_lvl ty
; ki_co <- uType kind_orig KindLevel ty_kind res_kind
; let ty_to_fill_with = ty `mkCastTy` ki_co
co = ty_co `mkTcCoherenceRightCo` ki_co
; when debugIsOn (check_hole ty_to_fill_with)
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
; writeTcRef ref (Just ty)
; when debugIsOn (check_hole ty_to_fill_with)
; writeTcRef ref (Just ty_to_fill_with)
; return co }
; return ty_co }
where
ty_kind = typeKind ty
kind_orig = TypeEqOrigin { uo_actual = ty_kind
, uo_expected = res_kind
, uo_thing = Nothing }
check_hole ty -- Debug check only
= do { ki1 <- zonkTcType (typeKind ty)
; ki2 <- zonkTcType res_kind
; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u )
; let ty_lvl = tcTypeLevel ty
= do { let ty_lvl = tcTypeLevel ty
; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
ppr u $$ ppr res_lvl $$ ppr ty_lvl )
ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
ppr ty <+> ppr (typeKind ty) $$ ppr orig_ty )
; cts <- readTcRef ref
; case cts of
Just already_there -> pprPanic "writeExpType"
......@@ -903,6 +894,121 @@ has the ir_inst flag.
else the outer visible type application won't work
-}
{- *********************************************************************
* *
Promoting types
* *
********************************************************************* -}
promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
-- See Note [Promoting a type]
-- promoteTcType level ty = (co, ty')
-- * Returns ty' whose max level is just 'level'
-- and whose kind is ~# to the kind of 'ty'
-- and whose kind has form TYPE rr
-- * and co :: ty ~ ty'
-- * and emits constraints to justify the coercion
promoteTcType dest_lvl ty
= do { cur_lvl <- getTcLevel
; if (cur_lvl `sameDepthAs` dest_lvl)
then dont_promote_it
else promote_it }
where
promote_it :: TcM (TcCoercion, TcType)
promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty
-- where alpha and rr are fresh and from level dest_lvl
= do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
; let eq_orig = TypeEqOrigin { uo_actual = ty
, uo_expected = prom_ty
, uo_thing = Nothing }
; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
; return (co, prom_ty) }
dont_promote_it :: TcM (TcCoercion, TcType)
dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
= do { res_kind <- newOpenTypeKind
; let ty_kind = typeKind ty
kind_orig = TypeEqOrigin { uo_actual = ty_kind
, uo_expected = res_kind
, uo_thing = Nothing }
; ki_co <- uType kind_orig KindLevel (typeKind ty) res_kind
; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co
; return (co, ty `mkCastTy` ki_co) }
{- Note [Promoting a type]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #12427)
data T where
MkT :: (Int -> Int) -> a -> T
h y = case y of MkT v w -> v
We'll infer the RHS type with an expected type ExpType of
(IR { ir_lvl = l, ir_ref = ref, ... )
where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern
match will increase the level, so we'll end up in tcSubType, trying to
unify the type of v,
v :: Int -> Int
with the expected type. But this attempt takes place at level (l+1),
rightly so, since v's type could have mentioned existential variables,
(like w's does) and we want to catch that.
So we
- create a new meta-var alpha[l+1]
- fill in the InferRes ref cell 'ref' with alpha
- emit an equality constraint, thus
[W] alpha[l+1] ~ (Int -> Int)
That constraint will float outwards, as it should, unless v's
type mentions a skolem-captured variable.
This approach fails if v has a higher rank type; see
Note [Promotion and higher rank types]
Note [Promotion and higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If v had a higher-rank type, say v :: (forall a. a->a) -> Int,
then we'd emit an equality
[W] alpha[l+1] ~ ((forall a. a->a) -> Int)
which will sadly fail because we can't unify a unification variable
with a polytype. But there is nothing really wrong with the program
here.
We could just about solve this by "promote the type" of v, to expose
its polymorphic "shape" while still leaving constraints that will
prevent existential escape. But we must be careful! Exposing
the "shape" of the type is precisely what we must NOT do under
a GADT pattern match! So in this case we might promote the type
to
(forall a. a->a) -> alpha[l+1]
and emit the constraint
[W] alpha[l+1] ~ Int
Now the poromoted type can fill the ref cell, while the emitted
equality can float or not, according to the usual rules.
But that's not quite right! We are exposing the arrow! We could
deal with that too:
(forall a. mu[l+1] a a) -> alpha[l+1]
with constraints
[W] alpha[l+1] ~ Int
[W] mu[l+1] ~ (->)
Here we abstract over the '->' inside the forall, in case that
is subject to an equality constraint from a GADT match.
Note that we kept the outer (->) becuase that's part of
the polymorphic "shape". And becauuse of impredicativity,
GADT matches can't give equalities that affect polymorphic
shape.
This reasoning just seems too complicated, so I decided not
to do it. These higher-rank notes are just here to record
the thinking.
-}
{- *********************************************************************
* *
Generalisation
......
gadt7.hs:16:38: error:
• Couldn't match expected type ‘p’ with actual type ‘p1’
‘p1’ is untouchable
‘p’ is untouchable
inside the constraints: a ~ Int
bound by a pattern with constructor: K :: T Int,
in a case alternative
at gadt7.hs:16:33
‘p1’ is a rigid type variable bound by
the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
‘p’ is a rigid type variable bound by
the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
‘p1’ is a rigid type variable bound by
the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
Possible fix: add a type signature for ‘i1b’
• In the expression: y1
In a case alternative: K -> y1
......
T2664.hs:31:52: error:
• Could not deduce: b ~ a arising from a use of ‘newPChan’
T2664.hs:31:9: error:
• Could not deduce: Dual a ~ Dual b
from the context: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
bound by the type signature for:
newPChan :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
IO (PChan (a :*: b), PChan c)
at T2664.hs:23:5-12
‘b’ is a rigid type variable bound by
the instance declaration at T2664.hs:22:10-52
‘a’ is a rigid type variable bound by
the instance declaration at T2664.hs:22:10-52
• In the third argument of ‘pchoose’, namely ‘newPChan’
In the first argument of ‘E’, namely ‘(pchoose Right v newPChan)’
Expected type: IO (PChan (a :*: b), PChan c)
Actual type: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
NB: ‘Dual’ is a type function, and may not be injective
• In a stmt of a 'do' block:
return
(O $ takeMVar v,
E (pchoose Right v newPChan) (pchoose Left v newPChan))
In the expression:
E (pchoose Right v newPChan) (pchoose Left v newPChan)
do { v <- newEmptyMVar;
return
(O $ takeMVar v,
E (pchoose Right v newPChan) (pchoose Left v newPChan)) }
In an equation for ‘newPChan’:
newPChan
= do { v <- newEmptyMVar;
return
(O $ takeMVar v,
E (pchoose Right v newPChan) (pchoose Left v newPChan)) }
• Relevant bindings include
v :: MVar (Either (PChan a) (PChan b)) (bound at T2664.hs:24:9)
newPChan :: IO (PChan (a :*: b), PChan c) (bound at T2664.hs:23:5)
T9662.hs:47:8: error:
• Couldn't match type ‘n’ with ‘Int’
n’ is a rigid type variable bound by
• Couldn't match type ‘k’ with ‘Int’
k’ is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
......
T7438.hs:6:14: error:
• Couldn't match expected type ‘p’ with actual type ‘p1’
‘p1’ is untouchable
‘p’ is untouchable
inside the constraints: b ~ a
bound by a pattern with constructor:
Nil :: forall k (a :: k). Thrist a a,
in an equation for ‘go’
at T7438.hs:6:4-6
‘p1’ is a rigid type variable bound by
the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
‘p’ is a rigid type variable bound by
the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
‘p1’ is a rigid type variable bound by
the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16
Possible fix: add a type signature for ‘go’
• In the expression: acc
In an equation for ‘go’: go Nil acc = acc
......
......@@ -11,8 +11,6 @@ T9222.hs:13:3: error:
forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
(a ~ '(b, c) => Proxy b) -> Want a
at T9222.hs:13:3
Expected type: Proxy b0
Actual type: Proxy b
• In the ambiguity check for ‘Want’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the definition of data constructor ‘Want’
......
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