Commit 7e96526a authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix TcSimplify.decideQuantification for kind variables

TcSimplify.decideQuantification was doing the Wrong Thing when
"growing" the type variables to quantify over. We were trying to do
this on a tyvar set where we'd split off the dependent type varaibles;
and we just got it wrong.  A kind variable wasn't being generalised
properly, with confusing knock on consequences.

All this led to Trac #13371 and Trac #13393.

This commit tidies it all up:

* The type TcDepVars is renamed as CandidateQTvs;
  and splitDepVarsOfType to candidateQTyVarsOfType

* The code in TcSimplify.decideQuantification is simpler.
  It no longer does the tricky "grow" stuff over TcDepVars.
  Instead it use ordinary VarSets (thereby eliminating the
  nasty growThetaTyVarsDSet) and uses that to filter the
  result of candidateQTyVarsOfType.

* I documented that candidateQTyVarsOfType returns the type
  variables in a good order in which to quantify, and rewrote
  it to use an accumulator pattern, so that we would predicatably
  get left-to-right ordering.

In doing all this I also made UniqDFM behave a little more nicely:

* When inserting an element that is there already, keep the old tag,
  while still overwriting with the new value.

* This means that when doing udfmToList we get back elements in the
  order they were originally inserted, rather than in reverse order.

It's not a big deal, but in a subsequent commit I use it to improve
the order of type variables in inferred types.

All this led to a lot of error message wibbles:
 - changing the order of quantified variables
 - changing the order in which instances are listed in GHCi
 - changing the tidying of variables in typechecker erors

There's a submodule update for 'array' because one of its tests
has an error-message change.

I may not have associated all of them with the correct commit.
parent bc0f3abd
......@@ -902,7 +902,7 @@ interface file. One such example is inferred type signatures. They also affect
the results of optimizations, for example worker-wrapper. This means that to
get deterministic builds quantifyTyVars needs to be deterministic.
To achieve this TcDepVars is backed by deterministic sets which allows them
To achieve this CandidatesQTvs is backed by deterministic sets which allows them
to be later converted to a list in a deterministic order.
For more information about deterministic sets see
......@@ -910,8 +910,8 @@ Note [Deterministic UniqFM] in UniqDFM.
-}
quantifyTyVars, quantifyZonkedTyVars
:: TcTyCoVarSet -- global tvs
-> TcDepVars -- See Note [Dependent type variables] in TcType
:: TcTyCoVarSet -- global tvs
-> CandidatesQTvs -- See Note [Dependent type variables] in TcType
-> TcM [TcTyVar]
-- See Note [quantifyTyVars]
-- Can be given a mixture of TcTyVars and TyVars, in the case of
......@@ -1257,15 +1257,15 @@ zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
zonkTcTypeAndFV ty
= tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
-- | Zonk a type and call 'splitDepVarsOfType' on it.
-- | Zonk a type and call 'candidateQTyVarsOfType' on it.
-- Works within the knot.
zonkTcTypeAndSplitDepVars :: TcType -> TcM TcDepVars
zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
zonkTcTypeAndSplitDepVars ty
= splitDepVarsOfType <$> zonkTcTypeInKnot ty
= candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM TcDepVars
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
zonkTcTypesAndSplitDepVars tys
= splitDepVarsOfTypes <$> mapM zonkTcTypeInKnot tys
= candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
zonkTyCoVar :: TyCoVar -> TcM TcType
-- Works on TyVars and TcTyVars
......
......@@ -808,17 +808,14 @@ decideQuantification
:: InferMode
-> [(Name, TcTauType)] -- Variables to be generalised
-> [PredType] -- All annotated constraints from signatures
-> [PredType] -- Candidate theta
-> [PredType] -- Candidate theta; already zonked
-> TcM ( [TcTyVar] -- Quantify over these (skolems)
, [PredType] ) -- and this context (fully zonked)
-- See Note [Deciding quantification]
decideQuantification infer_mode name_taus psig_theta candidates
= do { gbl_tvs <- tcGetGlobalTyCoVars
; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
-- psig_theta: see Note [Quantification and partial signatures]
; ovl_strings <- xoptM LangExt.OverloadedStrings
; let DV {dv_kvs = zkvs, dv_tvs = ztvs} = splitDepVarsOfTypes zonked_taus
(gbl_cand, quant_cand) -- gbl_cand = do not quantify me
= do { ovl_strings <- xoptM LangExt.OverloadedStrings
; gbl_tvs <- tcGetGlobalTyCoVars
; let (gbl_cand, quant_cand) -- gbl_cand = do not quantify me
= case infer_mode of -- quant_cand = try to quantify me
ApplyMR -> (candidates, [])
NoRestrictions -> ([], candidates)
......@@ -834,8 +831,20 @@ decideQuantification infer_mode name_taus psig_theta candidates
constrained_tvs = tyCoVarsOfTypes gbl_cand
mono_tvs = growThetaTyVars eq_constraints $
gbl_tvs `unionVarSet` constrained_tvs
tau_tvs_plus = growThetaTyVarsDSet quant_cand ztvs
dvs_plus = DV { dv_kvs = zkvs, dv_tvs = tau_tvs_plus }
; zonked_taus <- mapM TcM.zonkTcType (psig_theta ++ taus)
-- psig_theta: see Note [Quantification and partial signatures]
; let -- The candidate tyvars are the ones free in
-- either quant_cand or zonked_taus.
DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
= candidateQTyVarsOfTypes (quant_cand ++ zonked_taus)
-- Now keep only the ones reachable
-- (via growThetaTyVars) from zonked_taus.
grown_tvs = growThetaTyVars quant_cand (tyCoVarsOfTypes zonked_taus)
pick = filterDVarSet (`elemVarSet` grown_tvs)
dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
; qtvs <- quantifyZonkedTyVars mono_tvs dvs_plus
-- We don't grow the kvs, as there's no real need to. Recall
......@@ -855,7 +864,7 @@ decideQuantification infer_mode name_taus psig_theta candidates
-- Warn about the monomorphism restriction
; warn_mono <- woptM Opt_WarnMonomorphism
; let mr_bites | ApplyMR <- infer_mode
= constrained_tvs `intersectsVarSet` tcDepVarSet dvs_plus
= constrained_tvs `intersectsVarSet` grown_tvs
| otherwise
= False
; warnTc (Reason Opt_WarnMonomorphism) (warn_mono && mr_bites) $
......@@ -871,7 +880,8 @@ decideQuantification infer_mode name_taus psig_theta candidates
, text "quant_cand:" <+> ppr quant_cand
, text "gbl_tvs:" <+> ppr gbl_tvs
, text "mono_tvs:" <+> ppr mono_tvs
, text "tau_tvs_plus:" <+> ppr tau_tvs_plus
, text "cand_tvs" <+> ppr cand_tvs
, text "grown_tvs:" <+> ppr grown_tvs
, text "qtvs:" <+> ppr qtvs
, text "min_theta:" <+> ppr min_theta ])
; return (qtvs, min_theta) }
......@@ -901,32 +911,6 @@ growThetaTyVars theta tvs
where
pred_tvs = tyCoVarsOfType pred
------------------
growThetaTyVarsDSet :: ThetaType -> DTyCoVarSet -> DTyVarSet
-- See Note [Growing the tau-tvs using constraints]
-- NB: only returns tyvars, never covars
-- It takes a deterministic set of TyCoVars and returns a deterministic set
-- of TyVars.
-- The implementation mirrors growThetaTyVars, the only difference is that
-- it avoids unionDVarSet and uses more efficient extendDVarSetList.
growThetaTyVarsDSet theta tvs
| null theta = tvs_only
| otherwise = filterDVarSet isTyVar $
transCloDVarSet mk_next seed_tvs
where
tvs_only = filterDVarSet isTyVar tvs
seed_tvs = tvs `extendDVarSetList` tyCoVarsOfTypesList ips
(ips, non_ips) = partition isIPPred theta
-- See Note [Inheriting implicit parameters] in TcType
mk_next :: DVarSet -> DVarSet -- Maps current set to newly-grown ones
mk_next so_far = foldr (grow_one so_far) emptyDVarSet non_ips
grow_one so_far pred tvs
| any (`elemDVarSet` so_far) pred_tvs = tvs `extendDVarSetList` pred_tvs
| otherwise = tvs
where
pred_tvs = tyCoVarsOfTypeList pred
{- Note [Quantification and partial signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When choosing type variables to quantify, the basic plan is to
......
......@@ -103,7 +103,7 @@ module TcType (
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..),
anyRewritableTyVar,
-- * Extracting bound variables
......@@ -956,8 +956,8 @@ allBoundVariabless = mapUnionVarSet allBoundVariables
* *
********************************************************************* -}
data TcDepVars -- See Note [Dependent type variables]
-- See Note [TcDepVars determinism]
data CandidatesQTvs -- See Note [Dependent type variables]
-- See Note [CandidatesQTvs determinism]
= DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent)
, dv_tvs :: DTyVarSet -- "type" variables (non-dependent)
-- A variable may appear in both sets
......@@ -966,19 +966,14 @@ data TcDepVars -- See Note [Dependent type variables]
-- See Note [Dependent type variables]
}
tcDepVarSet :: TcDepVars -> TyVarSet
-- Actually can contain CoVars, but never mind
tcDepVarSet (DV { dv_kvs = kvs, dv_tvs = tvs })
= dVarSetToVarSet kvs `unionVarSet` dVarSetToVarSet tvs
instance Monoid TcDepVars where
instance Monoid CandidatesQTvs where
mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet }
mappend (DV { dv_kvs = kv1, dv_tvs = tv1 })
(DV { dv_kvs = kv2, dv_tvs = tv2 })
= DV { dv_kvs = kv1 `unionDVarSet` kv2
, dv_tvs = tv1 `unionDVarSet` tv2}
instance Outputable TcDepVars where
instance Outputable CandidatesQTvs where
ppr (DV {dv_kvs = kvs, dv_tvs = tvs })
= text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs
, text "dv_tvs =" <+> ppr tvs ])
......@@ -986,15 +981,22 @@ instance Outputable TcDepVars where
{- Note [Dependent type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In Haskell type inference we quantify over type variables; but we only
quantify over /kind/ variables when -XPolyKinds is on. So when
quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds
we default the kind variables to *.
So, to support this defaulting, and only for that reason, when
collecting the free vars of a type, prior to quantifying, we must keep
the type and kind variables separate. But what does that mean in a
system where kind variables /are/ type variables? It's a fairly
arbitrary distinction based on how the variables appear:
the type and kind variables separate.
But what does that mean in a system where kind variables /are/ type
variables? It's a fairly arbitrary distinction based on how the
variables appear:
- "Kind variables" appear in the kind of some other free variable
PLUS any free coercion variables
These are the ones we default to * if -XPolyKinds is off
- "Type variables" are all free vars that are not kind variables
E.g. In the type T k (a::k)
......@@ -1002,7 +1004,7 @@ E.g. In the type T k (a::k)
even though it also appears at "top level" of the type
'a' is a type variable, because it doesn't
We gather these variables using a TcDepVars record:
We gather these variables using a CandidatesQTvs record:
DV { dv_kvs: Variables free in the kind of a free type variable
or of a forall-bound type variable
, dv_tvs: Variables sytactically free in the type }
......@@ -1026,48 +1028,69 @@ Note that
The "type variables" do not depend on each other; if
one did, it'd be classified as a kind variable!
Note [TcDepVars determinism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we quantify over type variables we decide the order in which they
appear in the final type. Because the order of type variables in the type
can end up in the interface file and affects some optimizations like
worker-wrapper we want this order to be deterministic.
To achieve that we use deterministic sets of variables that can be converted to
lists in a deterministic order.
For more information about deterministic sets see
Note [Deterministic UniqFM] in UniqDFM.
Note [CandidatesQTvs determinism and order]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Determinism: when we quantify over type variables we decide the
order in which they appear in the final type. Because the order of
type variables in the type can end up in the interface file and
affects some optimizations like worker-wrapper, we want this order to
be deterministic.
To achieve that we use deterministic sets of variables that can be
converted to lists in a deterministic order. For more information
about deterministic sets see Note [Deterministic UniqFM] in UniqDFM.
* Order: as well as being deterministic, we use an
accumulating-parameter style for candidateQTyVarsOfType so that we
add variables one at a time, left to right. That means we tend to
produce the variables in left-to-right order. This is just to make
it bit more predicatable for the programmer.
-}
-- | Like 'splitDepVarsOfType', but over a list of types
splitDepVarsOfTypes :: [Type] -> TcDepVars
splitDepVarsOfTypes = foldMap splitDepVarsOfType
-- | Worker for 'splitDepVarsOfType'. This might output the same var
-- in both sets, if it's used in both a type and a kind.
-- See Note [TcDepVars determinism]
-- See Note [CandidatesQTvs determinism and order]
-- See Note [Dependent type variables]
splitDepVarsOfType :: Type -> TcDepVars
splitDepVarsOfType = go
candidateQTyVarsOfType :: Type -> CandidatesQTvs
candidateQTyVarsOfType = split_dvs emptyVarSet mempty
split_dvs :: VarSet -> CandidatesQTvs -> Type -> CandidatesQTvs
split_dvs bound dvs ty
= go dvs ty
where
go (TyVarTy tv) = DV { dv_kvs =tyCoVarsOfTypeDSet $ tyVarKind tv
, dv_tvs = unitDVarSet tv }
go (AppTy t1 t2) = go t1 `mappend` go t2
go (TyConApp _ tys) = foldMap go tys
go (FunTy arg res) = go arg `mappend` go res
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` go_co co
go (CoercionTy co) = go_co co
go (ForAllTy (TvBndr tv _) ty)
= let DV { dv_kvs = kvs, dv_tvs = tvs } = go ty in
DV { dv_kvs = (kvs `delDVarSet` tv)
`extendDVarSetList` tyCoVarsOfTypeList (tyVarKind tv)
, dv_tvs = tvs `delDVarSet` tv }
go_co co = DV { dv_kvs = tyCoVarsOfCoDSet co
go dv (AppTy t1 t2) = go (go dv t1) t2
go dv (TyConApp _ tys) = foldl go dv tys
go dv (FunTy arg res) = go (go dv arg) res
go dv (LitTy {}) = dv
go dv (CastTy ty co) = go dv ty `mappend` go_co co
go dv (CoercionTy co) = dv `mappend` go_co co
go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv)
| tv `elemVarSet` bound
= dv
| otherwise
= DV { dv_kvs = kvs `unionDVarSet`
kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
, dv_tvs = tvs `extendDVarSet` tv }
go dv (ForAllTy (TvBndr tv _) ty)
= DV { dv_kvs = kvs `unionDVarSet`
kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv))
, dv_tvs = tvs }
where
DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty
go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co)
, dv_tvs = emptyDVarSet }
kill_bound free
| isEmptyVarSet bound = free
| otherwise = filterDVarSet (not . (`elemVarSet` bound)) free
-- | Like 'splitDepVarsOfType', but over a list of types
candidateQTyVarsOfTypes :: [Type] -> CandidatesQTvs
candidateQTyVarsOfTypes = foldl (split_dvs emptyVarSet) mempty
{-
************************************************************************
* *
......
......@@ -143,34 +143,40 @@ unitUDFM :: Uniquable key => key -> elt -> UniqDFM elt
unitUDFM k v = UDFM (M.singleton (getKey $ getUnique k) (TaggedVal v 0)) 1
addToUDFM :: Uniquable key => UniqDFM elt -> key -> elt -> UniqDFM elt
addToUDFM (UDFM m i) k v =
UDFM (M.insert (getKey $ getUnique k) (TaggedVal v i) m) (i + 1)
addToUDFM m k v = addToUDFM_Directly m (getUnique k) v
addToUDFM_Directly :: UniqDFM elt -> Unique -> elt -> UniqDFM elt
addToUDFM_Directly (UDFM m i) u v =
UDFM (M.insert (getKey u) (TaggedVal v i) m) (i + 1)
addToUDFM_Directly_C
:: (elt -> elt -> elt) -> UniqDFM elt -> Unique -> elt -> UniqDFM elt
addToUDFM_Directly_C f (UDFM m i) u v =
UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1)
addToUDFM_Directly (UDFM m i) u v
= UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1)
where
tf (TaggedVal a j) (TaggedVal b _) = TaggedVal (f a b) j
tf (TaggedVal new_v _) (TaggedVal _ old_i) = TaggedVal new_v old_i
-- Keep the old tag, but insert the new value
-- This means that udfmToList typically returns elements
-- in the order of insertion, rather than the reverse
addListToUDFM :: Uniquable key => UniqDFM elt -> [(key,elt)] -> UniqDFM elt
addListToUDFM = foldl (\m (k, v) -> addToUDFM m k v)
addToUDFM_Directly_C
:: (elt -> elt -> elt) -- old -> new -> result
-> UniqDFM elt
-> Unique -> elt
-> UniqDFM elt
addToUDFM_Directly_C f (UDFM m i) u v
= UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1)
where
tf (TaggedVal new_v _) (TaggedVal old_v old_i)
= TaggedVal (f old_v new_v) old_i
-- Flip the arguments, because M.insertWith uses (new->old->result)
-- but f needs (old->new->result)
-- Like addToUDFM_Directly, keep the old tag
addToUDFM_C
:: Uniquable key => (elt -> elt -> elt) -- old -> new -> result
-> UniqDFM elt -- old
-> key -> elt -- new
-> UniqDFM elt -- result
addToUDFM_C f (UDFM m i) k v =
UDFM (M.insertWith tf (getKey $ getUnique k) (TaggedVal v i) m) (i + 1)
where
tf (TaggedVal a j) (TaggedVal b _) = TaggedVal (f b a) j
-- Flip the arguments, just like
-- addToUFM_C does.
addToUDFM_C f m k v = addToUDFM_Directly_C f m (getUnique k) v
addListToUDFM :: Uniquable key => UniqDFM elt -> [(key,elt)] -> UniqDFM elt
addListToUDFM = foldl (\m (k, v) -> addToUDFM m k v)
addListToUDFM_Directly :: UniqDFM elt -> [(Unique,elt)] -> UniqDFM elt
addListToUDFM_Directly = foldl (\m (k, v) -> addToUDFM_Directly m k v)
......
Subproject commit c58ecfadbe68486e9eab925c9c44d667316b2d14
Subproject commit 1b9a4430bbd6799f341a829f2d24ffc20e77ba2f
......@@ -4,33 +4,33 @@ TYPE SIGNATURES
test1a ::
forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
test2 ::
forall t b (f :: * -> *).
forall (f :: * -> *) t b.
(Num b, Num t, Applicative f) =>
(t -> f b) -> f b
test2a ::
forall t b (f :: * -> *).
forall (f :: * -> *) t b.
(Num b, Num t, Functor f) =>
(t -> f b) -> f b
test2b ::
forall (m :: * -> *) a t. (Num t, Monad m) => (t -> a) -> m a
forall (m :: * -> *) t a. (Num t, Monad m) => (t -> a) -> m a
test2c ::
forall t b (f :: * -> *).
forall (f :: * -> *) t b.
(Num b, Num t, Functor f) =>
(t -> f b) -> f b
test3 ::
forall a t1 (m :: * -> *) t2.
(Num t2, Monad m) =>
(t2 -> m t1) -> (t1 -> t1 -> m a) -> m a
forall (m :: * -> *) t1 t2 a.
(Num t1, Monad m) =>
(t1 -> m t2) -> (t2 -> t2 -> m a) -> m a
test4 ::
forall a1 a2 (m :: * -> *) t.
forall (m :: * -> *) t a1 a2.
(Num t, Monad m) =>
(t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
(t -> m a1) -> (a1 -> a1 -> m a2) -> m a2
test5 ::
forall a1 a2 (m :: * -> *) t.
forall (m :: * -> *) t a1 a2.
(Num t, Monad m) =>
(t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
(t -> m a1) -> (a1 -> a1 -> m a2) -> m a2
test6 ::
forall a (m :: * -> *) p.
forall (m :: * -> *) a p.
(Num (m a), Monad m) =>
(m a -> m (m a)) -> p -> m a
TYPE CONSTRUCTORS
......
[1 of 1] Compiling A ( A.hs, A.o )
TYPE SIGNATURES
test2 ::
forall t b (f :: * -> *).
forall (f :: * -> *) t b.
(Num b, Num t, Applicative f) =>
(t -> f b) -> f b
TYPE CONSTRUCTORS
......@@ -12,7 +12,7 @@ Dependent packages: [base-4.10.0.0, ghc-prim-0.5.0.0,
[1 of 1] Compiling A ( A.hs, A.o )
TYPE SIGNATURES
test2 ::
forall t b (f :: * -> *).
forall (f :: * -> *) t b.
(Num b, Num t, Applicative f) =>
(t -> f b) -> f b
TYPE CONSTRUCTORS
......
......@@ -17,7 +17,7 @@ werror.hs:10:1: warning: [-Wunused-top-binds (in -Wextra, -Wunused-binds)]
Defined but not used: ‘f’
werror.hs:10:1: warning: [-Wmissing-signatures (in -Wall)]
Top-level binding with no type signature: f :: [a2] -> [a1]
Top-level binding with no type signature: f :: [a1] -> [a2]
werror.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
......
gadt7.hs:16:38: error:
• Couldn't match expected type ‘p’ with actual type ‘p1
‘p’ is untouchable
• Couldn't match expected type ‘p1’ with actual type ‘p’
‘p1’ 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
‘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
the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
‘p’ is a rigid type variable bound by
the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44
Possible fix: add a type signature for ‘i1b’
• In the expression: y1
In a case alternative: K -> y1
In the expression: case t1 of { K -> y1 }
• Relevant bindings include
y1 :: p1 (bound at gadt7.hs:16:16)
y :: p1 (bound at gadt7.hs:16:7)
i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1)
y1 :: p (bound at gadt7.hs:16:16)
y :: p (bound at gadt7.hs:16:7)
i1b :: T a -> p -> p1 (bound at gadt7.hs:16:1)
Stopped in Test.foldl, break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t] -> Integer = _
xs :: [t] = _
go :: Integer -> [t1] -> Integer = _
xs :: [t1] = _
Stopped in Test.foldl.go, break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
......@@ -10,17 +10,17 @@ f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped in Test.foldl.go, break026.hs:7:23-35
_result :: t1 = _
c :: t1 = _
f :: t1 -> Integer -> t1 = _
_result :: t = _
c :: t = _
f :: t -> Integer -> t = _
x :: Integer = 2
xs :: [Integer] = _
c = 1
Stopped in Test.foldl, break026.hs:5:16-22
_result :: Integer = _
c :: Integer = 0
go :: Integer -> [t] -> Integer = _
xs :: [t] = _
go :: Integer -> [t1] -> Integer = _
xs :: [t1] = _
Stopped in Test.foldl.go, break026.hs:7:23-35
_result :: Integer = _
c :: Integer = 0
......@@ -28,9 +28,9 @@ f :: Integer -> Integer -> Integer = _
x :: Integer = 1
xs :: [Integer] = _
Stopped in Test.foldl.go, break026.hs:7:23-35
_result :: t1 = _
c :: t1 = _
f :: t1 -> Integer -> t1 = _
_result :: t = _
c :: t = _
f :: t -> Integer -> t = _
x :: Integer = 2
xs :: [Integer] = _
Stopped in Test.foldl.go, break026.hs:7:27-31
......
......@@ -6,8 +6,8 @@ pattern Pu :: p -> p -- Defined at <interactive>:18:1
pattern Pue :: a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1
pattern Pur :: (Num a, Eq a) => a -> [a]
-- Defined at <interactive>:20:1
pattern Purp :: (Num a1, Eq a1) => Show a => a1
-> a -> ([a1], UnivProv a)
pattern Purp :: (Num a, Eq a) => Show a1 => a
-> a1 -> ([a], UnivProv a1)
-- Defined at <interactive>:21:1
pattern Pure :: (Num a, Eq a) => a -> a1 -> ([a], Ex)
-- Defined at <interactive>:22:1
......@@ -31,8 +31,8 @@ pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
-- Defined at <interactive>:19:1
pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
-- Defined at <interactive>:20:1
pattern Purp :: forall {a} {a1}. (Num a1, Eq a1) => Show a => a1
-> a -> ([a1], UnivProv a)
pattern Purp :: forall {a} {a1}. (Num a, Eq a) => Show a1 => a
-> a1 -> ([a], UnivProv a1)
-- Defined at <interactive>:21:1
pattern Pure :: forall {a}. (Num a, Eq a) => forall {a1}. a
-> a1 -> ([a], Ex)
......
mapM
:: forall {t :: * -> *} {b} {m :: * -> *} {a}.
:: forall {t :: * -> *} {m :: * -> *} {a} {b}.
(Monad m, Traversable t) =>
(a -> m b) -> t a -> m (t b)
mapM
......
f :: forall {b} {a :: * -> *}. C a => a b
f :: forall {b} {a :: * -> *}. C a => a b
f :: forall {b} {a :: * -> *}. C a => a b
f :: forall {b} {a :: * -> *}. C a => a b
f :: forall {b} {a :: * -> *}. C a => a b
f :: forall {b} {a :: * -> *}. C a => a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
f ∷ ∀ {b} {a ∷ ★ → ★}. C a ⇒ a b
fmap ∷ ∀ {f ∷ ★ → ★} {b} {a}. Functor f ⇒ (a → b) → f a → f b
f :: forall {a :: * -> *} {b}. C a => a b
f :: forall {a :: * -> *} {b}. C a => a b
f :: forall {a :: * -> *} {b}. C a => a b
f :: forall {a :: * -> *} {b}. C a => a b
f :: forall {a :: * -> *} {b}. C a => a b
f :: forall {a :: * -> *} {b}. C a => a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
fmap ∷ ∀ {f ∷ ★ → ★} {a} {b}. Functor f ⇒ (a → b) → f a → f b
class Functor (f ∷ ★ → ★) where
fmap ∷ ∀ a b. (a → b) → f a → f b
...
......@@ -62,6 +62,6 @@ class Datatype (d ∷ k) where
t d f a → [Char]
...
-- Defined in ‘GHC.Generics’
(:*:) ∷ ∀ {g ∷ ★ → ★} {p} {f ∷ ★ → ★}. f p → g p → (:*:) f g p
(:*:) ∷ ∀ {f ∷ ★ → ★} {p} {g ∷ ★ → ★}. f p → g p → (:*:) f g p
Rep ∷ ★ → ★ → ★
M1 ∷ ∀ k. ★ → Meta → (k → ★) → k → ★
......@@ -4,8 +4,8 @@ type instance A Int Int = () -- Defined at T4175.hs:8:15
type instance A (B a) b = () -- Defined at T4175.hs:10:15
data family B a -- Defined at T4175.hs:12:1
instance G B -- Defined at T4175.hs:34:10
data instance B () = MkB -- Defined at T4175.hs:13:15
type instance A (B a) b = () -- Defined at T4175.hs:10:15
data instance B () = MkB -- Defined at T4175.hs:13:15