...
 
Commits (3)
  • Simon Peyton Jones's avatar
    Fail fast in solveLocalEqualities · a03619a0
    Simon Peyton Jones authored
    This patch makes us fail fast in TcSimplify.solveLocalEqualities,
    and in TcHsType.tc_hs_sig_type, if there are insoluble constraints.
    
    Previously we ploughed on even if there were insoluble constraints,
    leading to a cascade of hard-to-understand type errors. Failing
    eagerly is much better; hence a lot of testsuite error message
    changes.  Eg if we have
              f :: [Maybe] -> blah
              f xs = e
    then trying typecheck 'f x = e' with an utterly bogus type
    is just asking for trouble.
    
    I can't quite remember what provoked me to make this change,
    but I think the error messages are notably improved, by
    removing confusing clutter and focusing on the real error.
    
    (cherry picked from commit 5c1f268e)
    a03619a0
  • Richard Eisenberg's avatar
    Fix #16517 by bumping the TcLevel for method sigs · 5857463c
    Richard Eisenberg authored
    There were actually two bugs fixed here:
    
    1. candidateQTyVarsOfType needs to be careful that it does not
       try to zap metavariables from an outer scope as "naughty"
       quantification candidates. This commit adds a simple check
       to avoid doing so.
    
    2. We weren't bumping the TcLevel in kcHsKindSig, which was used
       only for class method sigs. This mistake led to the acceptance
       of
    
         class C a where
           meth :: forall k. Proxy (a :: k) -> ()
    
       Note that k is *locally* quantified. This patch fixes the
       problem by using tcClassSigType, which correctly bumps the
       level. It's a bit inefficient because tcClassSigType does other
       work, too, but it would be tedious to repeat much of the code
       there with only a few changes. This version works well and is
       simple.
    
    And, while updating comments, etc., I noticed that tcRnType was
    missing a pushTcLevel, leading to #16767, which this patch also
    fixes, by bumping the level. In the refactoring here, I also
    use solveEqualities. This initially failed ghci/scripts/T15415,
    but that was fixed by teaching solveEqualities to respect
    -XPartialTypeSignatures.
    
    This patch also cleans up some Notes around error generation that
    came up in conversation.
    
    Test case: typecheck/should_fail/T16517, ghci/scripts/T16767
    
    (cherry picked from commit a22e51ea)
    (cherry picked from commit 19ab32c5)
    5857463c
  • Ben Gamari's avatar
    ghci: Load static objects in batches · ce97ca46
    Ben Gamari authored
    Fixes #13786.
    ce97ca46
......@@ -389,8 +389,10 @@ linkCmdLineLibs' hsc_env pls =
all_paths_env <- addEnvPaths "LD_LIBRARY_PATH" all_paths
pathCache <- mapM (addLibrarySearchPath hsc_env) all_paths_env
let merged_specs = mergeStaticObjects cmdline_lib_specs
pls1 <- foldM (preloadLib hsc_env lib_paths framework_paths) pls
cmdline_lib_specs
merged_specs
maybePutStr dflags "final link ... "
ok <- resolveObjs hsc_env
......@@ -402,6 +404,19 @@ linkCmdLineLibs' hsc_env pls =
return pls1
-- | Merge runs of consecutive of 'Objects'. This allows for resolution of
-- cyclic symbol references when dynamically linking. Specifically, we link
-- together all of the static objects into a single shared object, avoiding
-- the issue we saw in #13786.
mergeStaticObjects :: [LibrarySpec] -> [LibrarySpec]
mergeStaticObjects specs = go [] specs
where
go :: [FilePath] -> [LibrarySpec] -> [LibrarySpec]
go accum (Objects objs : rest) = go (objs ++ accum) rest
go accum@(_:_) rest = Objects (reverse accum) : go [] rest
go [] (spec:rest) = spec : go [] rest
go [] [] = []
{- Note [preload packages]
Why do we need to preload packages from the command line? This is an
......@@ -429,7 +444,7 @@ users?
classifyLdInput :: DynFlags -> FilePath -> IO (Maybe LibrarySpec)
classifyLdInput dflags f
| isObjectFilename platform f = return (Just (Object f))
| isObjectFilename platform f = return (Just (Objects [f]))
| isDynLibFilename platform f = return (Just (DLLPath f))
| otherwise = do
putLogMsg dflags NoReason SevInfo noSrcSpan
......@@ -444,8 +459,8 @@ preloadLib
preloadLib hsc_env lib_paths framework_paths pls lib_spec = do
maybePutStr dflags ("Loading object " ++ showLS lib_spec ++ " ... ")
case lib_spec of
Object static_ish -> do
(b, pls1) <- preload_static lib_paths static_ish
Objects static_ishs -> do
(b, pls1) <- preload_statics lib_paths static_ishs
maybePutStrLn dflags (if b then "done" else "not found")
return pls1
......@@ -504,13 +519,13 @@ preloadLib hsc_env lib_paths framework_paths pls lib_spec = do
intercalate "\n" (map (" "++) paths)))
-- Not interested in the paths in the static case.
preload_static _paths name
= do b <- doesFileExist name
preload_statics _paths names
= do b <- or <$> mapM doesFileExist names
if not b then return (False, pls)
else if dynamicGhc
then do pls1 <- dynLoadObjs hsc_env pls [name]
then do pls1 <- dynLoadObjs hsc_env pls names
return (True, pls1)
else do loadObj hsc_env name
else do mapM_ (loadObj hsc_env) names
return (True, pls)
preload_static_archive _paths name
......@@ -1166,7 +1181,9 @@ unload_wkr hsc_env keep_linkables pls@PersistentLinkerState{..} = do
********************************************************************* -}
data LibrarySpec
= Object FilePath -- Full path name of a .o file, including trailing .o
= Objects [FilePath] -- Full path names of set of .o files, including trailing .o
-- We allow batched loading to ensure that cyclic symbol
-- references can be resolved (see #13786).
-- For dynamic objects only, try to find the object
-- file in all the directories specified in
-- v_Library_paths before giving up.
......@@ -1200,7 +1217,7 @@ partOfGHCi
["base", "template-haskell", "editline"]
showLS :: LibrarySpec -> String
showLS (Object nm) = "(static) " ++ nm
showLS (Objects nms) = "(static) [" ++ intercalate ", " nms ++ "]"
showLS (Archive nm) = "(static archive) " ++ nm
showLS (DLL nm) = "(dynamic) " ++ nm
showLS (DLLPath nm) = "(dynamic) " ++ nm
......@@ -1299,7 +1316,8 @@ linkPackage hsc_env pkg
-- Complication: all the .so's must be loaded before any of the .o's.
let known_dlls = [ dll | DLLPath dll <- classifieds ]
dlls = [ dll | DLL dll <- classifieds ]
objs = [ obj | Object obj <- classifieds ]
objs = [ obj | Objects objs <- classifieds
, obj <- objs ]
archs = [ arch | Archive arch <- classifieds ]
-- Add directories to library search paths
......@@ -1507,8 +1525,8 @@ locateLib hsc_env is_hs lib_dirs gcc_dirs lib
(ArchX86_64, OSSolaris2) -> "64" </> so_name
_ -> so_name
findObject = liftM (fmap Object) $ findFile dirs obj_file
findDynObject = liftM (fmap Object) $ findFile dirs dyn_obj_file
findObject = liftM (fmap $ Objects . (:[])) $ findFile dirs obj_file
findDynObject = liftM (fmap $ Objects . (:[])) $ findFile dirs dyn_obj_file
findArchive = let local name = liftM (fmap Archive) $ findFile dirs name
in apply (map local arch_files)
findHSDll = liftM (fmap DLLPath) $ findFile dirs hs_dyn_lib_file
......
......@@ -2079,13 +2079,6 @@ What do we do when we have an equality
where k1 and k2 differ? This Note explores this treacherous area.
First off, the question above is slightly the wrong question. Flattening
a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
the kind might introduce a cast. So we might have a casted tyvar on the
left. We thus revise our test case to
(tv |> co :: k1) ~ (rhs :: k2)
We must proceed differently here depending on whether we have a Wanted
or a Given. Consider this:
......@@ -2109,36 +2102,33 @@ The reason for this odd behavior is much the same as
Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
new `co` is a Wanted.
The solution is then not to use `co` to "rewrite" -- that is, cast
-- `w`, but instead to keep `w` heterogeneous and
irreducible. Given that we're not using `co`, there is no reason to
collect evidence for it, so `co` is born a Derived, with a CtOrigin
of KindEqOrigin.
The solution is then not to use `co` to "rewrite" -- that is, cast -- `w`, but
instead to keep `w` heterogeneous and irreducible. Given that we're not using
`co`, there is no reason to collect evidence for it, so `co` is born a
Derived, with a CtOrigin of KindEqOrigin. When the Derived is solved (by
unification), the original wanted (`w`) will get kicked out. We thus get
When the Derived is solved (by unification), the original wanted (`w`)
will get kicked out.
[D] _ :: k ~ Type
[W] w :: (alpha :: k) ~ (Int :: Type)
Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
trigger, because flattening would have rewritten k to Type. That is,
`w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
case will trigger, correctly rewriting alpha to (Int |> sym co1).
Note that the Wanted is unchanged and will be irreducible. This all happens
in canEqTyVarHetero.
Note that, if we had [G] co1 :: k ~ Type available, then we never get
to canEqTyVarHetero: canEqTyVar tries flattening the kinds first. If
we have [G] co1 :: k ~ Type, then flattening the kind of alpha would
rewrite k to Type, and we would end up in canEqTyVarHomo.
Successive canonicalizations of the same Wanted may produce
duplicate Deriveds. Similar duplications can happen with fundeps, and there
seems to be no easy way to avoid. I expect this case to be rare.
For Givens, this problem doesn't bite, so a heterogeneous Given gives
For Givens, this problem (the Wanteds-rewriting-Wanteds action of
a kind coercion) doesn't bite, so a heterogeneous Given gives
rise to a Given kind equality. No Deriveds here. We thus homogenise
the Given (see the "homo_co" in the Given case in canEqTyVar) and
the Given (see the "homo_co" in the Given case in canEqTyVarHetero) and
carry on with a homogeneous equality constraint.
Separately, I (Richard E) spent some time pondering what to do in the case
that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
differ. Note that the tv is the same. (This case is handled as the first
case in canEqTyVarHomo.) At one point, I thought we could solve this limited
form of heterogeneous Wanted, but I then reconsidered and now treat this case
just like any other heterogeneous Wanted.
Note [Type synonyms and canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We treat type synonym applications as xi types, that is, they do not
......
......@@ -158,14 +158,22 @@ reportUnsolved wanted
-- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
-- However, do not make any evidence bindings, because we don't
-- have any convenient place to put them.
-- NB: Type-level holes are OK, because there are no bindings.
-- See Note [Deferring coercion errors to runtime]
-- Used by solveEqualities for kind equalities
-- (see Note [Fail fast on kind errors] in TcSimplify]
-- (see Note [Fail fast on kind errors] in TcSimplify)
-- and for simplifyDefault.
reportAllUnsolved :: WantedConstraints -> TcM ()
reportAllUnsolved wanted
= do { ev_binds <- newNoTcEvBinds
; report_unsolved TypeError HoleError HoleError HoleError
; partial_sigs <- xoptM LangExt.PartialTypeSignatures
; warn_partial_sigs <- woptM Opt_WarnPartialTypeSignatures
; let type_holes | not partial_sigs = HoleError
| warn_partial_sigs = HoleWarn
| otherwise = HoleDefer
; report_unsolved TypeError HoleError type_holes HoleError
ev_binds wanted }
-- | Report all unsolved goals as warnings (but without deferring any errors to
......
......@@ -11,7 +11,7 @@
module TcHsType (
-- Type signatures
kcHsSigType, tcClassSigType,
kcClassSigType, tcClassSigType,
tcHsSigType, tcHsSigWcType,
tcHsPartialSigType,
funsSigCtxt, addSigCtxt, pprSigCtxt,
......@@ -187,24 +187,40 @@ tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type
-- already checked this, so we can simply ignore it.
tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty)
kcHsSigType :: [Located Name] -> LHsSigType GhcRn -> TcM ()
kcHsSigType names (HsIB { hsib_body = hs_ty
, hsib_ext = sig_vars })
= addSigCtxt (funsSigCtxt names) hs_ty $
discardResult $
bindImplicitTKBndrs_Skol sig_vars $
tc_lhs_type typeLevelMode hs_ty liftedTypeKind
kcHsSigType _ (XHsImplicitBndrs _) = panic "kcHsSigType"
kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM ()
kcClassSigType skol_info names sig_ty
= discardResult $
tcClassSigType skol_info names sig_ty
-- tcClassSigType does a fair amount of extra work that we don't need,
-- such as ordering quantified variables. But we absolutely do need
-- to push the level when checking method types and solve local equalities,
-- and so it seems easier just to call tcClassSigType than selectively
-- extract the lines of code from tc_hs_sig_type that we really need.
-- If we don't push the level, we get #16517, where GHC accepts
-- class C a where
-- meth :: forall k. Proxy (a :: k) -> ()
-- Note that k is local to meth -- this is hogwash.
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
-- Does not do validity checking
tcClassSigType skol_info names sig_ty
= addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
-- Do not zonk-to-Type, nor perform a validity check
-- We are in a knot with the class and associated types
-- Zonking and validity checking is done by tcClassDecl
-- No need to fail here if the type has an error:
-- If we're in the kind-checking phase, the solveEqualities
-- in kcTyClGroup catches the error
-- If we're in the type-checking phase, the solveEqualities
-- in tcClassDecl1 gets it
-- Failing fast here degrades the error message in, e.g., tcfail135:
-- class Foo f where
-- baa :: f a -> f
-- If we fail fast, we're told that f has kind `k1` when we wanted `*`.
-- It should be that f has kind `k2 -> *`, but we never get a chance
-- to run the solver where the kind of f is touchable. This is
-- painfully delicate.
tcHsSigType :: UserTypeCtxt -> LHsSigType GhcRn -> TcM Type
-- Does validity checking
......@@ -214,10 +230,13 @@ tcHsSigType ctxt sig_ty
do { traceTc "tcHsSigType {" (ppr sig_ty)
-- Generalise here: see Note [Kind generalisation]
; ty <- tc_hs_sig_type skol_info sig_ty
(expectedKindInCtxt ctxt)
; (insol, ty) <- tc_hs_sig_type skol_info sig_ty
(expectedKindInCtxt ctxt)
; ty <- zonkTcType ty
; when insol failM
-- See Note [Fail fast if there are insoluble kind equalities] in TcSimplify
; checkValidType ctxt ty
; traceTc "end tcHsSigType }" (ppr ty)
; return ty }
......@@ -225,12 +244,14 @@ tcHsSigType ctxt sig_ty
skol_info = SigTypeSkol ctxt
tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
-> ContextKind -> TcM Type
-> ContextKind -> TcM (Bool, TcType)
-- Kind-checks/desugars an 'LHsSigType',
-- solve equalities,
-- and then kind-generalizes.
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking or zonking
-- Returns also a Bool indicating whether the type induced an insoluble constraint;
-- True <=> constraint is insoluble
tc_hs_sig_type skol_info hs_sig_type ctxt_kind
| HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
= do { (tc_lvl, (wanted, (spec_tkvs, ty)))
......@@ -249,9 +270,9 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
tc_lvl wanted
; return (mkInvForAllTys kvs ty1) }
; return (insolubleWC wanted, mkInvForAllTys kvs ty1) }
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
......@@ -2056,7 +2077,8 @@ kindGeneralize :: TcType -> TcM [KindVar]
-- Quantify the free kind variables of a kind or type
-- In the latter case the type is closed, so it has no free
-- type variables. So in both cases, all the free vars are kind vars
-- Input needn't be zonked.
-- Input needn't be zonked. All variables to be quantified must
-- have a TcLevel higher than the ambient TcLevel.
-- NB: You must call solveEqualities or solveLocalEqualities before
-- kind generalization
--
......@@ -2074,7 +2096,8 @@ kindGeneralize kind_or_type
-- | This variant of 'kindGeneralize' refuses to generalize over any
-- variables free in the given WantedConstraints. Instead, it promotes
-- these variables into an outer TcLevel. See also
-- these variables into an outer TcLevel. All variables to be quantified must
-- have a TcLevel higher than the ambient TcLevel. See also
-- Note [Promoting unification variables] in TcSimplify
kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar]
kindGeneralizeLocal wanted kind_or_type
......
......@@ -759,14 +759,14 @@ writeMetaTyVar tyvar ty
-- Everything from here on only happens if DEBUG is on
| not (isTcTyVar tyvar)
= WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
= ASSERT2( False, text "Writing to non-tc tyvar" <+> ppr tyvar )
return ()
| MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
= writeMetaTyVarRef tyvar ref ty
| otherwise
= WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
= ASSERT2( False, text "Writing to non-meta tyvar" <+> ppr tyvar )
return ()
--------------------
......@@ -1066,18 +1066,18 @@ we are trying to generalise this type:
forall arg. ... (alpha[tau]:arg) ...
We have a metavariable alpha whose kind mentions a skolem variable
boudn inside the very type we are generalising.
bound inside the very type we are generalising.
This can arise while type-checking a user-written type signature
(see the test case for the full code).
We cannot generalise over alpha! That would produce a type like
forall {a :: arg}. forall arg. ...blah...
The fact that alpha's kind mentions arg renders it completely
ineligible for generaliation.
ineligible for generalisation.
However, we are not going to learn any new constraints on alpha,
because its kind isn't even in scope in the outer context. So alpha
is entirely unconstrained.
because its kind isn't even in scope in the outer context (but see Wrinkle).
So alpha is entirely unconstrained.
What then should we do with alpha? During generalization, every
metavariable is either (A) promoted, (B) generalized, or (C) zapped
......@@ -1098,6 +1098,17 @@ We do this eager zapping in candidateQTyVars, which always precedes
generalisation, because at that moment we have a clear picture of
what skolems are in scope.
Wrinkle:
We must make absolutely sure that alpha indeed is not
from an outer context. (Otherwise, we might indeed learn more information
about it.) This can be done easily: we just check alpha's TcLevel.
That level must be strictly greater than the ambient TcLevel in order
to treat it as naughty. We say "strictly greater than" because the call to
candidateQTyVars is made outside the bumped TcLevel, as stated in the
comment to candidateQTyVarsOfType. The level check is done in go_tv
in collect_cant_qtvs. Skipping this check caused #16517.
-}
data CandidatesQTvs
......@@ -1145,13 +1156,17 @@ candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs)
-- | Gathers free variables to use as quantification candidates (in
-- 'quantifyTyVars'). This might output the same var
-- in both sets, if it's used in both a type and a kind.
-- The variables to quantify must have a TcLevel strictly greater than
-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
-- See Note [CandidatesQTvs determinism and order]
-- See Note [Dependent type variables]
candidateQTyVarsOfType :: TcType -- not necessarily zonked
-> TcM CandidatesQTvs
candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty
-- | Like 'splitDepVarsOfType', but over a list of types
-- | Like 'candidateQTyVarsOfType', but over a list of types
-- The variables to quantify must have a TcLevel strictly greater than
-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates])
candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs
candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys
......@@ -1175,7 +1190,7 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars
collect_cand_qtvs
:: Bool -- True <=> consider every fv in Type to be dependent
-> VarSet -- Bound variables (both locally bound and globally bound)
-> VarSet -- Bound variables (locals only)
-> CandidatesQTvs -- Accumulating parameter
-> Type -- Not necessarily zonked
-> TcM CandidatesQTvs
......@@ -1220,16 +1235,26 @@ collect_cand_qtvs is_dep bound dvs ty
-----------------
go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
| tv `elemDVarSet` kvs = return dv -- We have met this tyvar aleady
| tv `elemDVarSet` kvs
= return dv -- We have met this tyvar aleady
| not is_dep
, tv `elemDVarSet` tvs = return dv -- We have met this tyvar aleady
, tv `elemDVarSet` tvs
= return dv -- We have met this tyvar aleady
| otherwise
= do { tv_kind <- zonkTcType (tyVarKind tv)
-- This zonk is annoying, but it is necessary, both to
-- ensure that the collected candidates have zonked kinds
-- (Trac #15795) and to make the naughty check
-- (which comes next) works correctly
; if intersectsVarSet bound (tyCoVarsOfType tv_kind)
; cur_lvl <- getTcLevel
; if tcTyVarLevel tv `strictlyDeeperThan` cur_lvl &&
-- this tyvar is from an outer context: see Wrinkle
-- in Note [Naughty quantification candidates]
intersectsVarSet bound (tyCoVarsOfType tv_kind)
then -- See Note [Naughty quantification candidates]
do { traceTc "Zapping naughty quantifier" (pprTyVar tv)
......
......@@ -2427,12 +2427,13 @@ tcRnType hsc_env normalise rdr_type
-- It can have any rank or kind
-- First bring into scope any wildcards
; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
; ((ty, kind), lie) <-
captureConstraints $
; (ty, kind) <- pushTcLevelM_ $
-- must push level to satisfy level precondition of
-- kindGeneralize, below
solveEqualities $
tcWildCardBinders wcs $ \ wcs' ->
do { emitWildCardHoleConstraints wcs'
; tcLHsTypeUnsaturated rn_type }
; _ <- checkNoErrs (simplifyInteractive lie)
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kind <- zonkTcType kind
......
......@@ -2095,6 +2095,16 @@ see dropDerivedWC. For example
[D] Int ~ Bool, and we don't want to report that because it's
incomprehensible. That is why we don't rewrite wanteds with wanteds!
* We might float out some Wanteds from an implication, leaving behind
their insoluble Deriveds. For example:
forall a[2]. [W] alpha[1] ~ Int
[W] alpha[1] ~ Bool
[D] Int ~ Bool
The Derived is insoluble, but we very much want to drop it when floating
out.
But (tiresomely) we do keep *some* Derived constraints:
* Type holes are derived constraints, because they have no evidence
......@@ -2103,8 +2113,7 @@ But (tiresomely) we do keep *some* Derived constraints:
* Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with
KindEqOrigin, may arise from a type equality a ~ Int#, say. See
Note [Equalities with incompatible kinds] in TcCanonical.
These need to be kept because the kind equalities might have different
source locations and hence different error messages.
Keeping these around produces better error messages, in practice.
E.g., test case dependent/should_fail/T11471
* We keep most derived equalities arising from functional dependencies
......
......@@ -152,8 +152,26 @@ solveLocalEqualities :: String -> TcM a -> TcM a
solveLocalEqualities callsite thing_inside
= do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside
; emitConstraints wanted
-- See Note [Fail fast if there are insoluble kind equalities]
; when (insolubleWC wanted) $
failM
; return res }
{- Note [Fail fast if there are insoluble kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Rather like in simplifyInfer, fail fast if there is an insoluble
constraint. Otherwise we'll just succeed in kind-checking a nonsense
type, with a cascade of follow-up errors.
For example polykinds/T12593, T15577, and many others.
Take care to ensure that you emit the insoluble constraints before
failing, because they are what will ulimately lead to the error
messsage!
-}
solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a)
solveLocalEqualitiesX callsite thing_inside
= do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ])
......
......@@ -1038,9 +1038,11 @@ kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
do { _ <- tcHsContext ctxt
; mapM_ (wrapLocM_ kc_sig) sigs }
where
kc_sig (ClassOpSig _ _ nms op_ty) = kcHsSigType nms op_ty
kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty
kc_sig _ = return ()
skol_info = TyConSkol ClassFlavour name
kcTyClDecl (FamDecl _ (FamilyDecl { fdLName = (dL->L _ fam_tc_name)
, fdInfo = fd_info }))
-- closed type families look at their equations, but other families don't
......
......@@ -516,6 +516,17 @@ superSkolemTv = SkolemTv topTcLevel True -- Treat this as a completely disti
-- The choice of level number here is a bit dodgy, but
-- topTcLevel works in the places that vanillaSkolemTv is used
instance Outputable TcTyVarDetails where
ppr = pprTcTyVarDetails
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl
pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
= ppr info <> colon <> ppr tclvl
-----------------------------
data MetaDetails
= Flexi -- Flexi type variables unify to become Indirects
......@@ -544,20 +555,11 @@ instance Outputable MetaDetails where
ppr Flexi = text "Flexi"
ppr (Indirect ty) = text "Indirect" <+> ppr ty
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
pprTcTyVarDetails (RuntimeUnk {}) = text "rt"
pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl
pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
= pp_info <> colon <> ppr tclvl
where
pp_info = case info of
TauTv -> text "tau"
TyVarTv -> text "tyv"
FlatMetaTv -> text "fmv"
FlatSkolTv -> text "fsk"
instance Outputable MetaInfo where
ppr TauTv = text "tau"
ppr TyVarTv = text "tyv"
ppr FlatMetaTv = text "fmv"
ppr FlatSkolTv = text "fsk"
{- *********************************************************************
* *
......@@ -795,10 +797,10 @@ checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
= ctxt_tclvl >= tv_tclvl
-- Returns topTcLevel for non-TcTyVars
tcTyVarLevel :: TcTyVar -> TcLevel
tcTyVarLevel tv
= ASSERT2( tcIsTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
= case tcTyVarDetails tv of
MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
SkolemTv tv_lvl _ -> tv_lvl
RuntimeUnk -> topTcLevel
......
......@@ -4,23 +4,7 @@ DepFail1.hs:7:6: error:
Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’
• In the type signature: z :: Proxy Bool
DepFail1.hs:8:5: error:
• Couldn't match expected type ‘Proxy Bool’
with actual type ‘Proxy k0 a1’
• In the expression: P
In an equation for ‘z’: z = P
DepFail1.hs:10:16: error:
• Expected kind ‘Int’, but ‘Bool’ has kind ‘*’
• In the second argument of ‘Proxy’, namely ‘Bool’
In the type signature: a :: Proxy Int Bool
DepFail1.hs:11:5: error:
• Couldn't match kind ‘*’ with ‘Int’
When matching types
a0 :: Int
Bool :: *
Expected type: Proxy Int Bool
Actual type: Proxy Int a0
• In the expression: P
In an equation for ‘a’: a = P
<interactive>:3:1: error:
• Couldn't match kind ‘()’ with ‘*’
When matching types
a0 :: *
'() :: ()
• In the expression: undefined :: '()
In an equation for ‘it’: it = undefined :: '()
<interactive>:3:14: error:
• Expected a type, but ‘'()’ has kind ‘()’
• In an expression type signature: '()
......@@ -19,34 +11,14 @@
In the expression: undefined :: Proxy '() Int
In an equation for ‘it’: it = undefined :: Proxy '() Int
<interactive>:5:1: error:
• Couldn't match kind ‘[*]’ with ‘*’
When matching types
a0 :: *
'[(), ()] :: [*]
• In the expression: undefined :: [(), ()]
In an equation for ‘it’: it = undefined :: [(), ()]
<interactive>:5:14: error:
• Expected a type, but ‘[(), ()]’ has kind ‘[*]’
• In an expression type signature: [(), ()]
In the expression: undefined :: [(), ()]
In an equation for ‘it’: it = undefined :: [(), ()]
<interactive>:6:1: error:
• Couldn't match kind ‘([k0], [k1])’ with ‘*’
When matching types
a0 :: *
'( '[], '[]) :: ([k0], [k1])
• In the expression: undefined :: '( '[], '[])
In an equation for ‘it’: it = undefined :: '( '[], '[])
• Relevant bindings include
it :: '( '[], '[]) (bound at <interactive>:6:1)
<interactive>:6:14: error:
• Expected a type, but ‘'( '[], '[])’ has kind ‘([k0], [k1])’
• In an expression type signature: '( '[], '[])
In the expression: undefined :: '( '[], '[])
In an equation for ‘it’: it = undefined :: '( '[], '[])
• Relevant bindings include
it :: '( '[], '[]) (bound at <interactive>:6:1)
:set -fprint-explicit-foralls -fprint-explicit-kinds -XTypeApplications -XDataKinds
import Data.Proxy
:kind! 'Proxy @_
'Proxy @_ :: forall {k} {_ :: k}. Proxy @{k} _
= 'Proxy @{k} @_
......@@ -296,3 +296,4 @@ test('T16030', normal, ghci_script, ['T16030.script'])
test('T11606', normal, ghci_script, ['T11606.script'])
test('T16089', normal, ghci_script, ['T16089.script'])
test('T16527', normal, ghci_script, ['T16527.script'])
test('T16767', normal, ghci_script, ['T16767.script'])
T13877.hs:65:17: error:
• Couldn't match type ‘Apply p (x : xs)’ with ‘p (x : xs)’
Expected type: Sing x
-> Sing xs
-> App [a1] (':->) * p xs
-> App [a1] (':->) * p (x : xs)
Actual type: Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs)
• In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
listElimTyFun = listElimPoly @(:->) @a @p @l
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a1) (xs :: [a1]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T13877.hs:65:41: error:
• Expecting one more argument to ‘p’
Expected kind ‘(-?>) [a1] * (':->)’, but ‘p’ has kind ‘[a1] ~> *’
Expected kind ‘(-?>) [a] * (':->)’, but ‘p’ has kind ‘[a] ~> *’
• In the type ‘p’
In the expression: listElimPoly @(:->) @a @p @l
In an equation for ‘listElimTyFun’:
......@@ -27,7 +9,7 @@ T13877.hs:65:41: error:
• Relevant bindings include
listElimTyFun :: Sing l
-> (p @@ '[])
-> (forall (x :: a1) (xs :: [a1]).
-> (forall (x :: a) (xs :: [a]).
Sing x -> Sing xs -> (p @@ xs) -> p @@ (x : xs))
-> p @@ l
(bound at T13877.hs:65:1)
T11976.hs:7:7: error:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls: Lens _3 _4 _5
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined :: Lens _ _ _
In an equation for ‘foo’: foo = undefined :: Lens _ _ _
• Relevant bindings include
foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
T11976.hs:7:20: error:
• Expected kind ‘k0 -> *’, but ‘Lens _ _’ has kind ‘*’
• In the type ‘Lens _ _ _’
In an expression type signature: Lens _ _ _
In the expression: undefined :: Lens _ _ _
• Relevant bindings include
foo :: Lens _ _1 _2 (bound at T11976.hs:7:1)
T12634.hs:14:19: error:
• Found type wildcard ‘_’ standing for ‘()’
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
bench_twacePow :: forall t m m' r.
_ => t m' r -> Bench '(t, m, m', r)
T12634.hs:14:58: error:
• Expected a type, but
‘'(t, m, m', r)’ has kind
‘(* -> * -> *, *, *, *)’
‘(k1 -> k2 -> *, k0, k1, k2)’
• In the first argument of ‘Bench’, namely ‘'(t, m, m', r)’
In the type ‘t m' r -> Bench '(t, m, m', r)’
In the type signature:
bench_twacePow :: forall t m m' r.
_ => t m' r -> Bench '(t, m, m', r)
T12634.hs:15:18: error:
• Couldn't match kind ‘(* -> * -> *, *, *, *)’ with ‘*’
When matching types
params0 :: *
'(t, m, m', r) :: (* -> * -> *, *, *, *)
Expected type: t m' r -> Bench '(t, m, m', r)
Actual type: t m' r -> Bench params0
• In the expression: bench (twacePowDec :: t m' r -> t m r)
In an equation for ‘bench_twacePow’:
bench_twacePow = bench (twacePowDec :: t m' r -> t m r)
• Relevant bindings include
bench_twacePow :: t m' r -> Bench '(t, m, m', r)
(bound at T12634.hs:15:1)
T15289.hs:5:16: error:
• Couldn't match expected type ‘Maybe’ with actual type ‘Bool’
• In the pattern: True
In the pattern: True :: Maybe
In the declaration for pattern synonym ‘What’
T15289.hs:5:24: error:
• Expecting one more argument to ‘Maybe’
Expected a type, but ‘Maybe’ has kind ‘* -> *’
......
T12593.hs:11:16: error:
• Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’
• In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:31: error:
• Expecting one more argument to ‘k’
Expected a type, but
‘k’ has kind
‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint’
‘((k0 -> Constraint) -> k1 -> *) -> Constraint’
• In the kind ‘k’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:40: error:
• Expecting two more arguments to ‘k1’
Expected a type, but
‘k1’ has kind
‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’
• In the kind ‘k1’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:47: error:
• Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *)
-> Constraint’
with ‘*’
When matching kinds
k3 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the first argument of ‘p’, namely ‘c’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:49: error:
• Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *’
with ‘*’
When matching kinds
k4 :: *
k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
• In the second argument of ‘p’, namely ‘d’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:56: error:
• Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *)
-> Constraint’
with ‘*’
When matching kinds
k0 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the first argument of ‘q’, namely ‘c’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:12:58: error:
• Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint)
-> (k3 -> k4 -> *) -> *’
with ‘*’
When matching kinds
k1 :: *
k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *
• In the second argument of ‘q’, namely ‘d’
In the type signature:
run :: k2 q =>
Free k k1 k2 p a b
-> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
T12593.hs:14:6: error:
• Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’
Expected type: Free k6 k7 k8 p a b
Actual type: Free k2 p0 a b
• In the pattern: Free cat
In an equation for ‘run’: run (Free cat) = cat
• Relevant bindings include
run :: Free k k4 k8 p a b
-> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
T12593.hs:14:18: error:
• Couldn't match kind ‘*’
with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint’
When matching kinds
k0 :: *
k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *)
-> Constraint
• In the expression: cat
In an equation for ‘run’: run (Free cat) = cat
• Relevant bindings include
cat :: forall (q :: k0 -> k1 -> *).
k2 q =>
(forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b
(bound at T12593.hs:14:11)
run :: Free k k4 k8 p a b
-> (forall (c :: k) (d :: k4). p c d -> q c d) -> q a b
(bound at T12593.hs:14:1)
......@@ -7,65 +7,3 @@ T15577.hs:20:18: error:
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
T15577.hs:20:21: error:
• Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
• In the type ‘a’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:20:24: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
f1 a1 :: *
Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’
• In the type ‘r’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:20:26: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching kinds
f1 :: * -> *
a1 :: *
• In the fourth argument of ‘f’, namely ‘r’
In a stmt of a pattern guard for
an equation for ‘g’:
Refl <- f @f @a @r r
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
T15577.hs:21:7: error:
• Could not deduce: F r1 ~ r1
from the context: r0 ~ F r0
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a pattern binding in
a pattern guard for
an equation for ‘g’
at T15577.hs:18:7-10
‘r1’ is a rigid type variable bound by
the type signature for:
g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
Proxy r1 -> F r1 :~: r1
at T15577.hs:17:1-76
Expected type: F r1 :~: r1
Actual type: r1 :~: r1
• In the expression: Refl
In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
• Relevant bindings include
r :: Proxy r1 (bound at T15577.hs:18:3)
g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
......@@ -2,12 +2,3 @@
T11112.hs:3:9: error:
• Expected a type, but ‘Ord s’ has kind ‘Constraint’
• In the type signature: sort :: Ord s -> [s] -> [s]
T11112.hs:4:11: error:
• Couldn't match expected type ‘[s] -> [s]’
with actual type ‘Ord s’
• In the expression: xs
In an equation for ‘sort’: sort xs = xs
• Relevant bindings include
xs :: Ord s (bound at T11112.hs:4:6)
sort :: Ord s => [s] -> [s] (bound at T11112.hs:4:1)
T13819.hs:12:10: error:
• Couldn't match type ‘_0 -> A _0’ with ‘A a’
Expected type: a -> A a
Actual type: (_1 -> WrappedMonad A _2) (_0 -> A _0)
• In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
In an equation for ‘pure’:
pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
In the instance declaration for ‘Applicative A’
• Relevant bindings include
pure :: a -> A a (bound at T13819.hs:12:3)
T13819.hs:12:17: error:
• Expected kind ‘* -> *’, but ‘_ -> WrappedMonad A _’ has kind ‘*’
• In the type ‘(_ -> WrappedMonad A _)’
......
......@@ -2,16 +2,3 @@
T14232.hs:3:6: error:
• Expected kind ‘* -> *’, but ‘String -> a’ has kind ‘*’
• In the type signature: f :: (String -> a) String -> a
T14232.hs:4:9: error:
• Couldn't match type ‘String -> a’ with ‘(->) t0’
Expected type: t0 -> [Char]
Actual type: (String -> a) String
• The function ‘g’ is applied to one argument,
but its type ‘(String -> a) String’ has none
In the expression: g s
In an equation for ‘f’: f g s = g s
• Relevant bindings include
s :: t0 (bound at T14232.hs:4:5)
g :: (String -> a) String (bound at T14232.hs:4:3)
f :: (String -> a) String -> a (bound at T14232.hs:4:1)
{-# LANGUAGE PolyKinds #-}
module T16517 where
import Data.Proxy
class C a where m :: Proxy (a :: k)
T16517.hs:5:29: error:
• Expected kind ‘k’, but ‘a’ has kind ‘k0’
• In the first argument of ‘Proxy’, namely ‘(a :: k)’
In the type signature: m :: Proxy (a :: k)
In the class declaration for ‘C’
......@@ -3,16 +3,6 @@ T3540.hs:4:12: error:
• Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
• In the type signature: thing :: (a ~ Int)
T3540.hs:5:9: error:
• Couldn't match kind ‘Constraint’ with ‘*’
When matching types
a0 :: *
a ~ Int :: Constraint
• In the expression: undefined
In an equation for ‘thing’: thing = undefined
• Relevant bindings include
thing :: a ~ Int (bound at T3540.hs:5:1)
T3540.hs:7:20: error:
• Expected a type, but ‘a ~ Int’ has kind ‘Constraint’
• In the type signature: thing1 :: Int -> (a ~ Int)
......
T7778.hs:3:6: error:
• Illegal qualified type: Num Int => Num
A constraint must be a monotype
Perhaps you intended to use QuantifiedConstraints
• In the type signature: v :: ((Num Int => Num) ()) => ()
T7778.hs:3:7: error:
• Expected kind ‘* -> Constraint’,
but ‘Num Int => Num’ has kind ‘*’
......
T8806.hs:5:6: error:
• Expected a constraint, but ‘Int’ has kind ‘*’
• In the type signature:
f :: Int => Int
• In the type signature: f :: Int => Int
T8806.hs:8:7: error:
• Expected a constraint, but ‘Int’ has kind ‘*’
• In the type signature:
g :: (Int => Show a) => Int
• In the type signature: g :: (Int => Show a) => Int
......@@ -25,17 +25,6 @@ VtaFail.hs:26:15: error:
In the expression: first @Int F
In an equation for ‘fInt’: fInt = first @Int F
VtaFail.hs:26:19: error:
• Couldn't match kind ‘*’ with ‘* -> *’
When matching types
a1 :: * -> *
Int :: *
Expected type: First Int
Actual type: First a1
• In the second argument of ‘first’, namely ‘F’
In the expression: first @Int F
In an equation for ‘fInt’: fInt = first @Int F
VtaFail.hs:33:18: error:
• Couldn't match type ‘Int’ with ‘Bool’
Expected type: Proxy Bool
......@@ -50,17 +39,6 @@ VtaFail.hs:40:17: error:
In the expression: too @Maybe T
In an equation for ‘threeBad’: threeBad = too @Maybe T
VtaFail.hs:40:23: error:
• Couldn't match kind ‘*’ with ‘k0 -> *’
When matching types
a0 :: * -> k0 -> *
Maybe :: * -> *
Expected type: Three Maybe
Actual type: Three a0
• In the second argument of ‘too’, namely ‘T’
In the expression: too @Maybe T
In an equation for ‘threeBad’: threeBad = too @Maybe T
VtaFail.hs:41:27: error:
• Couldn't match type ‘Either’ with ‘(->)’
Expected type: Three (->)
......
......@@ -511,3 +511,4 @@ test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
['T16059e', '-v0'])
test('T16255', normal, compile_fail, [''])
test('T16204c', normal, compile_fail, [''])
test('T16517', normal, compile_fail, [''])
......@@ -2,12 +2,3 @@
tcfail057.hs:5:7: error:
• Expected a type, but ‘RealFrac a’ has kind ‘Constraint’
• In the type signature: f :: (RealFrac a) -> a -> a
tcfail057.hs:6:7: error:
• Couldn't match expected type ‘a -> a’
with actual type ‘RealFrac a’
• In the expression: x
In an equation for ‘f’: f x = x
• Relevant bindings include
x :: RealFrac a (bound at tcfail057.hs:6:3)
f :: RealFrac a => a -> a (bound at tcfail057.hs:6:1)
......@@ -3,23 +3,3 @@ tcfail058.hs:6:7: error:
• Expecting one more argument to ‘Array a’
Expected a constraint, but ‘Array a’ has kind ‘* -> *’
• In the type signature: f :: (Array a) => a -> b
tcfail058.hs:7:7: error:
• Could not deduce: a ~ b
from the context: Array a
bound by the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
‘b’ is a rigid type variable bound by
the type signature for:
f :: forall a b. Array a => a -> b
at tcfail058.hs:6:1-24
• In the expression: x
In an equation for ‘f’: f x = x
• Relevant bindings include
x :: a (bound at tcfail058.hs:7:3)
f :: a -> b (bound at tcfail058.hs:7:1)
......@@ -3,20 +3,3 @@ tcfail063.hs:6:9: error:
• Expecting one more argument to ‘Num’
Expected a constraint, but ‘Num’ has kind ‘* -> Constraint’
• In the type signature: moby :: Num => Int -> a -> Int
tcfail063.hs:7:14: error:
• Could not deduce: a ~ Int
from the context: Num
bound by the type signature for:
moby :: forall a. Num => Int -> a -> Int
at tcfail063.hs:6:1-30
‘a’ is a rigid type variable bound by
the type signature for:
moby :: forall a. Num => Int -> a -> Int
at tcfail063.hs:6:1-30
• In the second argument of ‘(+)’, namely ‘y’
In the expression: x + y
In an equation for ‘moby’: moby x y = x + y
• Relevant bindings include
y :: a (bound at tcfail063.hs:7:8)
moby :: Int -> a -> Int (bound at tcfail063.hs:7:1)
......@@ -4,32 +4,11 @@ tcfail113.hs:12:7: error:
Expected a type, but ‘Maybe’ has kind ‘* -> *’
• In the type signature: f :: [Maybe]
tcfail113.hs:13:1: error:
• Couldn't match expected type ‘[Maybe]’
with actual type ‘p1 -> p1’
• The equation(s) for ‘f’ have one argument,
but its type ‘[Maybe]’ has none
• Relevant bindings include
f :: [Maybe] (bound at tcfail113.hs:13:1)
tcfail113.hs:15:8: error:
• Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type signature: g :: T Int
tcfail113.hs:16:1: error:
• Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
• The equation(s) for ‘g’ have one argument,
but its type ‘T Int’ has none
• Relevant bindings include g :: T Int (bound at tcfail113.hs:16:1)
tcfail113.hs:18:6: error:
• Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
• In the type signature: h :: Int Int
tcfail113.hs:19:1: error:
• Couldn't match type ‘Int’ with ‘(->) Int’
Expected type: Int Int
Actual type: Int -> Int
• The equation(s) for ‘h’ have one argument,
but its type ‘Int Int’ has none
......@@ -2,6 +2,5 @@
tcfail134.hs:5:33: error:
• Expecting one more argument to ‘XML’
Expected a type, but ‘XML’ has kind ‘* -> Constraint’
• In the type signature:
toXML :: a -> XML
• In the type signature: toXML :: a -> XML
In the class declaration for ‘XML’
......@@ -3,9 +3,3 @@ tcfail160.hs:7:8: error:
• Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
• In the first argument of ‘T’, namely ‘Int’
In the type signature: g :: T Int
tcfail160.hs:8:1: error:
• Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’
• The equation(s) for ‘g’ have one argument,
but its type ‘T Int’ has none
• Relevant bindings include g :: T Int (bound at tcfail160.hs:8:1)
......@@ -3,11 +3,3 @@ tcfail161.hs:5:7: error:
• Expecting one more argument to ‘Maybe’
Expected a type, but ‘Maybe’ has kind ‘* -> *’
• In the type signature: f :: [Maybe]
tcfail161.hs:6:1: error:
• Couldn't match expected type ‘[Maybe]’
with actual type ‘p0 -> p0’
• The equation(s) for ‘f’ have one argument,
but its type ‘[Maybe]’ has none
• Relevant bindings include
f :: [Maybe] (bound at tcfail161.hs:6:1)
......@@ -9,20 +9,6 @@ tcfail212.hs:10:14: error:
Expected a type, but ‘Either Int’ has kind ‘* -> *’
• In the type signature: f :: (Maybe, Either Int)
tcfail212.hs:11:6: error:
• Couldn't match expected type ‘Maybe’
with actual type ‘Maybe Integer’
• In the expression: Just 1
In the expression: (Just 1, Left 1)
In an equation for ‘f’: f = (Just 1, Left 1)
tcfail212.hs:11:14: error:
• Couldn't match expected type ‘Either Int’
with actual type ‘Either Integer b0’
• In the expression: Left 1
In the expression: (Just 1, Left 1)
In an equation for ‘f’: f = (Just 1, Left 1)
tcfail212.hs:13:7: error:
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the type signature: g :: (Int#, Int#)
......@@ -30,3 +16,25 @@ tcfail212.hs:13:7: error:
tcfail212.hs:13:13: error:
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the type signature: g :: (Int#, Int#)
tcfail212.hs:14:6: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a :: *
Int# :: TYPE 'IntRep
• In the expression: 1#
In the expression: (1#, 2#)
In an equation for ‘g’: g = (1#, 2#)
• Relevant bindings include
g :: (a, b) (bound at tcfail212.hs:14:1)
tcfail212.hs:14:10: error:
• Couldn't match a lifted type with an unlifted type
When matching types
b :: *
Int# :: TYPE 'IntRep
• In the expression: 2#
In the expression: (1#, 2#)
In an equation for ‘g’: g = (1#, 2#)
• Relevant bindings include
g :: (a, b) (bound at tcfail212.hs:14:1)