Commit e0c433c8 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #13337.

The big change is the introduction of solveSomeEqualities. This
is just like solveEqualities, but it doesn't fail if there are unsolved
equalities when it's all done. Anything unsolved is re-emitted. This
is appropriate if we are not kind-generalizing, so this new form
is used when decideKindGeneralizationPlan says not to.

We initially thought that any use of solveEqualities would be tied
to kind generalization, but this isn't true. For example, we need
to solveEqualities a bunch in the "tc" pass in TcTyClsDecls (which
is really desugaring). These equalities are all surely going to be
soluble (if they weren't the "kc" pass would fail), but we still
need to solve them again. Perhaps if the "kc" pass produced type-
checked output that is then desugared, solveEqualities really would
be tied only to kind generalization.

Updates haddock submodule.

Test Plan: ./validate, typecheck/should_compile/T13337

Reviewers: simonpj, bgamari, austin

Reviewed By: simonpj

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3315
parent 4b673e80
......@@ -513,7 +513,7 @@ cvtConstr (ForallC tvs ctxt con)
let hs_ty = mkHsForAllTy tvs noSrcSpan tvs' rho_ty
rho_ty = mkHsQualTy ctxt noSrcSpan (L loc ctxt')
(hsib_body conT)
in con' { con_type = HsIB PlaceHolder hs_ty }
in con' { con_type = mkHsImplicitBndrs hs_ty }
ConDeclH98 {} ->
let qvars = case (tvs, con_qvars con') of
([], Nothing) -> Nothing
......
......@@ -1088,7 +1088,7 @@ instance (OutputableBndrId name)
-- This complexity is to distinguish between
-- deriving Show
-- deriving (Show)
pp_dct [a@(HsIB _ (L _ HsAppsTy{}))] = parens (ppr a)
pp_dct [a@(HsIB { hsib_body = L _ HsAppsTy{} })] = parens (ppr a)
pp_dct [a] = ppr a
pp_dct _ = parens (interpp'SP dct)
......
......@@ -290,6 +290,9 @@ isEmptyLHsQTvs _ = False
data HsImplicitBndrs name thing -- See Note [HsType binders]
= HsIB { hsib_vars :: PostRn name [Name] -- Implicitly-bound kind & type vars
, hsib_body :: thing -- Main payload (type or list of types)
, hsib_closed :: PostRn name Bool -- Taking the hsib_vars into account,
-- is the payload closed? Used in
-- TcHsType.decideKindGeneralisationPlan
}
-- | Haskell Wildcard Binders
......@@ -306,7 +309,7 @@ data HsWildCardBndrs name thing
-- it's still there in the hsc_body.
}
deriving instance (Data name, Data thing, Data (PostRn name [Name]))
deriving instance (Data name, Data thing, Data (PostRn name [Name]), Data (PostRn name Bool))
=> Data (HsImplicitBndrs name thing)
deriving instance (Data name, Data thing, Data (PostRn name [Name]))
......@@ -357,8 +360,9 @@ the explicitly forall'd tyvar 'a' is bound by the HsForAllTy
-}
mkHsImplicitBndrs :: thing -> HsImplicitBndrs RdrName thing
mkHsImplicitBndrs x = HsIB { hsib_body = x
, hsib_vars = PlaceHolder }
mkHsImplicitBndrs x = HsIB { hsib_body = x
, hsib_vars = PlaceHolder
, hsib_closed = PlaceHolder }
mkHsWildCardBndrs :: thing -> HsWildCardBndrs RdrName thing
mkHsWildCardBndrs x = HsWC { hswc_body = x
......@@ -367,8 +371,9 @@ mkHsWildCardBndrs x = HsWC { hswc_body = x
-- Add empty binders. This is a bit suspicious; what if
-- the wrapped thing had free type variables?
mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs Name thing
mkEmptyImplicitBndrs x = HsIB { hsib_body = x
, hsib_vars = [] }
mkEmptyImplicitBndrs x = HsIB { hsib_body = x
, hsib_vars = []
, hsib_closed = False }
mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs Name thing
mkEmptyWildCardBndrs x = HsWC { hswc_body = x
......
......@@ -777,7 +777,8 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload
; return (tycon',
HsIB { hsib_body = pats'
, hsib_vars = all_ibs },
, hsib_vars = all_ibs
, hsib_closed = True },
payload',
all_fvs) }
-- type instance => use, hence addOneFV
......
......@@ -110,7 +110,7 @@ rn_hs_sig_wc_type no_implicit_if_forall ctxt
; rnImplicitBndrs no_implicit_if_forall tv_rdrs hs_ty $ \ vars ->
do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
; let sig_ty' = HsWC { hswc_wcs = wcs, hswc_body = ib_ty' }
ib_ty' = HsIB { hsib_vars = vars, hsib_body = hs_ty' }
ib_ty' = mk_implicit_bndrs vars hs_ty' fvs1
; (res, fvs2) <- thing_inside sig_ty'
; return (res, fvs1 `plusFV` fvs2) } }
......@@ -247,8 +247,7 @@ rnHsSigType ctx (HsIB { hsib_body = hs_ty })
= do { vars <- extractFilteredRdrTyVars hs_ty
; rnImplicitBndrs True vars hs_ty $ \ vars ->
do { (body', fvs) <- rnLHsType ctx hs_ty
; return (HsIB { hsib_vars = vars
, hsib_body = body' }, fvs) } }
; return ( mk_implicit_bndrs vars body' fvs, fvs ) } }
rnImplicitBndrs :: Bool -- True <=> no implicit quantification
-- if type is headed by a forall
......@@ -292,6 +291,15 @@ rnLHsInstType doc_str inst_ty
text "Malformed instance:" <+> ppr inst_ty
; rnHsSigType (GenericCtx doc_str) inst_ty }
mk_implicit_bndrs :: [Name] -- implicitly bound
-> a -- payload
-> FreeVars -- FreeVars of payload
-> HsImplicitBndrs Name a
mk_implicit_bndrs vars body fvs
= HsIB { hsib_vars = vars
, hsib_body = body
, hsib_closed = nameSetAll (not . isTyVarName) (vars `delFVs` fvs) }
{- ******************************************************
* *
......
......@@ -321,8 +321,7 @@ tcHsBootSigs binds sigs
tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
where
f (L _ name)
= do { sigma_ty <- solveEqualities $
tcHsSigWcType (FunSigCtxt name False) hs_ty
= do { sigma_ty <- tcHsSigWcType (FunSigCtxt name False) hs_ty
; return (mkVanillaGlobal name sigma_ty) }
-- Notice that we make GlobalIds, not LocalIds
tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
......
......@@ -240,7 +240,7 @@ tcFImport :: LForeignDecl Name -> TcM (Id, LForeignDecl Id, Bag GlobalRdrElt)
tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty
, fd_fi = imp_decl }))
= setSrcSpan dloc $ addErrCtxt (foreignDeclCtxt fo) $
do { sig_ty <- solveEqualities $ tcHsSigType (ForSigCtxt nm) hs_ty
do { sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
; (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
; let
-- Drop the foralls before inspecting the
......
......@@ -5,7 +5,7 @@
\section[TcMonoType]{Typechecking user-specified @MonoTypes@}
-}
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
{-# LANGUAGE CPP, TupleSections, MultiWayIf, RankNTypes #-}
module TcHsType (
-- Type signatures
......@@ -53,7 +53,7 @@ import TcMType
import TcValidity
import TcUnify
import TcIface
import TcSimplify ( solveEqualities )
import TcSimplify ( solveEqualities, solveSomeEqualities )
import TcType
import TcHsSyn( zonkSigType )
import Inst ( tcInstBinders, tcInstBindersX, tcInstBinderX )
......@@ -190,8 +190,7 @@ tcClassSigType :: [Located Name] -> LHsSigType Name -> TcM Type
-- the recursive class declaration "knot"
tcClassSigType names sig_ty
= addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
do { ty <- tc_hs_sig_type sig_ty liftedTypeKind
; kindGeneralizeType ty }
tc_hs_sig_type_and_gen sig_ty liftedTypeKind
tcHsSigType :: UserTypeCtxt -> LHsSigType Name -> TcM Type
-- Does validity checking
......@@ -204,22 +203,37 @@ tcHsSigType ctxt sig_ty
-- The kind is checked by checkValidType, and isn't necessarily
-- of kind * in a Template Haskell quote eg [t| Maybe |]
; ty <- tc_hs_sig_type sig_ty kind
-- Generalise here: see Note [Kind generalisation]
; do_kind_gen <- decideKindGeneralisationPlan ty
; do_kind_gen <- decideKindGeneralisationPlan sig_ty
; ty <- if do_kind_gen
then kindGeneralizeType ty
else zonkTcType ty
then tc_hs_sig_type_and_gen sig_ty kind
else tc_hs_sig_type sig_ty kind >>= zonkTcType
; checkValidType ctxt ty
; return ty }
-- kind-checks/desugars an 'LHsSigType' and then kind-generalizes.
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking, but it does zonk en route to generalization
tc_hs_sig_type_and_gen :: LHsSigType Name -> Kind -> TcM Type
tc_hs_sig_type_and_gen sig_ty kind
= do { ty <- tc_hs_sig_type_x solveEqualities sig_ty kind
; kindGeneralizeType ty }
tc_hs_sig_type :: LHsSigType Name -> Kind -> TcM Type
-- Does not do validity checking or zonking
tc_hs_sig_type (HsIB { hsib_body = hs_ty
, hsib_vars = sig_vars }) kind
= do { (tkvs, ty) <- solveEqualities $
-- May emit constraints; uses solveSomeEqualities internally.
-- No zonking or validity checking
tc_hs_sig_type = tc_hs_sig_type_x solveSomeEqualities
-- Version of tc_hs_sig_type parameterized over how it should solve
-- equalities
tc_hs_sig_type_x :: (forall a. TcM a -> TcM a) -- solveSomeEqualities
-- or solveEqualities
-> LHsSigType Name -> Kind
-> TcM Type
tc_hs_sig_type_x solve (HsIB { hsib_body = hs_ty
, hsib_vars = sig_vars }) kind
= do { (tkvs, ty) <- solve $
tcImplicitTKBndrsType sig_vars $
tc_lhs_type typeLevelMode hs_ty kind
; return (mkSpecForAllTys tkvs ty) }
......@@ -237,8 +251,7 @@ tcHsDeriv hs_ty
-- can be no covars in an outer scope
; ty <- checkNoErrs $
-- avoid redundant error report with "illegal deriving", below
tc_hs_sig_type hs_ty cls_kind
; ty <- kindGeneralizeType ty -- also zonks
tc_hs_sig_type_and_gen hs_ty cls_kind
; cls_kind <- zonkTcType cls_kind
; let (tvs, pred) = splitForAllTys ty
; let (args, _) = splitFunTys cls_kind
......@@ -252,8 +265,7 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
-- Like tcHsSigType, but for a class instance declaration
tcHsClsInstType user_ctxt hs_inst_ty
= setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
do { inst_ty <- tc_hs_sig_type hs_inst_ty constraintKind
; inst_ty <- kindGeneralizeType inst_ty
do { inst_ty <- tc_hs_sig_type_and_gen hs_inst_ty constraintKind
; checkValidInstance user_ctxt hs_inst_ty inst_ty }
-- Used for 'VECTORISE [SCALAR] instance' declarations
......@@ -276,7 +288,9 @@ tcHsVectInst ty
tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type
tcHsTypeApp wc_ty kind
| HsWC { hswc_wcs = sig_wcs, hswc_body = hs_ty } <- wc_ty
= do { ty <- solveEqualities $
-- use solveSomeEqualities b/c we are in an expression
-- See Note [solveEqualities vs solveSomeEqualities] in TcSimplify
= do { ty <- solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ _ ->
tcCheckLHsType hs_ty kind
; ty <- zonkTcType ty
......@@ -290,8 +304,8 @@ tcHsTypeApp wc_ty kind
************************************************************************
* *
The main kind checker: no validity checks here
%* *
%************************************************************************
* *
************************************************************************
First a couple of simple wrappers for kcHsType
-}
......@@ -320,18 +334,14 @@ tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
---------------------------
-- | Should we generalise the kind of this type signature?
-- We *should* generalise if the type mentions no scoped type variables
-- We *should* generalise if the type is closed
-- or if NoMonoLocalBinds is set. Otherwise, nope.
decideKindGeneralisationPlan :: Type -> TcM Bool
decideKindGeneralisationPlan ty
decideKindGeneralisationPlan :: LHsSigType Name -> TcM Bool
decideKindGeneralisationPlan sig_ty@(HsIB { hsib_closed = closed })
= do { mono_locals <- xoptM LangExt.MonoLocalBinds
; in_scope <- getInLocalScope
; let fvs = tyCoVarsOfTypeList ty
should_gen = not mono_locals || all (not . in_scope . getName) fvs
; let should_gen = not mono_locals || closed
; traceTc "decideKindGeneralisationPlan"
(vcat [ text "type:" <+> ppr ty
, text "ftvs:" <+> ppr fvs
, text "should gen?" <+> ppr should_gen ])
(ppr sig_ty $$ text "should gen?" <+> ppr should_gen)
; return should_gen }
{-
......@@ -1771,13 +1781,16 @@ the term:
* We instantiate the explicit and implicit foralls with SigTvs
* We instantiate the wildcards with meta tyvars
We /do/ call solveEqualities, and then zonk to propage the result of
solveEqualities, mainly so that functions like matchExpectedFunTys will
We /do/ call solveSomeEqualities, and then zonk to propagate the result of
solveSomeEqualities, mainly so that functions like matchExpectedFunTys will
be able to decompose the type, and hence higher-rank signatures will
work. Ugh! For example
f :: (forall a. a->a) -> _
f x = (x True, x 'c')
Because we are not generalizing, etc., solveSomeEqualities is appropriate.
See also Note [solveEqualities vs solveSomeEqualities] in TcSimplify.
-}
tcHsPartialSigType
......@@ -1795,7 +1808,7 @@ tcHsPartialSigType ctxt sig_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (wcs, wcx, explicit_tvs, theta, tau))
<- -- See Note [Solving equalities in partial type signatures]
solveEqualities $
solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
tcImplicitTKBndrsX new_implicit_tv implicit_hs_tvs $
tcExplicitTKBndrsX newSigTyVar explicit_hs_tvs $ \ explicit_tvs ->
......@@ -1857,7 +1870,7 @@ tcHsPatSigType ctxt sig_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (wcs, sig_ty))
<- -- See Note [Solving equalities in partial type signatures]
solveEqualities $
solveSomeEqualities $
tcWildCardBindersX newWildTyVar sig_wcs $ \ wcs ->
tcImplicitTKBndrsX new_implicit_tv sig_vars $
do { sig_ty <- tcHsOpenType hs_ty
......
......@@ -6,7 +6,7 @@ module TcSimplify(
simplifyAmbiguityCheck,
simplifyDefault,
simplifyTop, simplifyTopImplic, captureTopConstraints,
simplifyInteractive, solveEqualities,
simplifyInteractive, solveSomeEqualities, solveEqualities,
simplifyWantedsTcM,
tcCheckSatisfiability,
......@@ -128,8 +128,68 @@ simplifyTop wanteds
; return (evBindMapBinds binds1 `unionBags` binds2) }
{- Note [solveEqualities vs solveSomeEqualities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking a type, GHC might generate equality constraints. (We know
it will generate only *equalities*, not e.g. class constraints, because types
don't contain class methods.) What should we do with these constraints?
Before we can effectively zonk, generalize, or validity-check a type, we need
to solve these equalities. The functions solveEqualities and solveSomeEqualities
do precisely this.
solveEqualities solves *all* equality constraints generated by the thing_inside.
If any constraints are unable to be solved, fail. This is appropriate for a top-
level type where we absolutely must, say, generalize right away. For example,
in
data G (a :: k) where
MkG :: G Maybe
The type G Maybe will make equality constraints that must be handled pronto.
solveSomeEqualities, on the other hand, does the best it can, re-emitting those
constraints it can't solve. This is appropriate when, for example, a type
appears in the middle of an expression (either a type annotation or a visible
type application) and there may be givens that have a bearing on whether or
not a type-level equality is soluble. The use of solveEqualities in an type
annotation is what gave rise to #13337.
Why have solveSomeEqualities at all, instead of just letting all equality
constraints go where all the other constraints do? Because we want to nail what
equalities we can before doing validity checking. Otherwise, the validity checker
may see casts and other nonsense in what should be a simple type.
How to choose between these?
Use solveEqualities when any of the following apply:
* you are about to kind-generalize
* you are about to call zonkTcTypeToType
* you are in a top-level context, not inside of any expression
Use solveSomeEqualities when:
* none of the above applies
-}
-- | Type-check a thing that emits only equality constraints, then
-- solve as many constraints as possible. Re-emits any unsolved constraints.
-- Never fails. This is useful when you're in a context where emitting
-- constraints is a good idea (e.g., in a expression type signature) but
-- you also want to use a function from TcValidity. TcValidity wants the
-- type to be as well-defined as possible. So this does what it can.
-- See also Note [solveEqualities vs solveSomeEqualities]
solveSomeEqualities :: TcM a -> TcM a
solveSomeEqualities thing_inside
= do { (result, wanted) <- captureConstraints thing_inside
; traceTc "solveSomeEqualities {" $ text "wanted = " <+> ppr wanted
; final_wc <- runTcSEqualities $ simpl_top wanted
; traceTc "End solveESomequalities }" empty
; emitConstraints final_wc
; return result }
-- | Type-check a thing that emits only equality constraints, then
-- solve those constraints. Fails outright if there is trouble.
-- See also Note [solveEqualities vs solveSomeEqualities]
solveEqualities :: TcM a -> TcM a
solveEqualities thing_inside
= checkNoErrs $ -- See Note [Fail fast on kind errors]
......
......@@ -1066,7 +1066,8 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
-- Typecheck RHS
; let pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
, hsib_body = map hsLTyVarBndrToType exp_vars }
, hsib_body = map hsLTyVarBndrToType exp_vars
, hsib_closed = False } -- this field is ignored, anyway
-- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
-- the LHsQTyVars used for declaring a tycon, but the names here
-- are different.
......
......@@ -92,7 +92,8 @@
(HsTyVar
(NotPromoted)
({ DumpParsedAst.hs:8:15-16 }
(Unqual {OccName: as}))))))]))))])
(Unqual {OccName: as}))))))]))))]
(PlaceHolder))
(Prefix)
({ DumpParsedAst.hs:8:21-36 }
(HsAppsTy
......@@ -136,7 +137,8 @@
(HsExplicitListTy
(Promoted)
(PlaceHolder)
[]))])
[]))]
(PlaceHolder))
(Prefix)
({ DumpParsedAst.hs:9:21-24 }
(HsAppsTy
......
......@@ -118,7 +118,8 @@
({ DumpRenamedAst.hs:8:15-16 }
(HsTyVar
(NotPromoted)
({ DumpRenamedAst.hs:8:15-16 }{Name: as{tv}})))))))])
({ DumpRenamedAst.hs:8:15-16 }{Name: as{tv}})))))))]
(True))
(Prefix)
({ DumpRenamedAst.hs:8:21-36 }
(HsAppTy
......@@ -148,7 +149,8 @@
(HsExplicitListTy
(Promoted)
(PlaceHolder)
[]))])
[]))]
(True))
(Prefix)
({ DumpRenamedAst.hs:9:21-24 }
(HsTyVar
......
T11976.hs:7:20: error:
• Illegal polymorphic type: Lens w0 w1
GHC doesn't yet support impredicative polymorphism
• In an expression type signature: Lens _ _ _
In the expression: undefined :: Lens _ _ _
In an equation for ‘foo’: foo = undefined :: Lens _ _ _
T11976.hs:7:20: error:
• Expecting one fewer arguments to ‘Lens w0 w1’
Expected kind ‘k0 -> *’, but ‘Lens w0 w1’ has kind ‘*’
......
T12634.hs:14:37: error:
• Found type wildcard ‘_’ standing for ‘() :: Constraint’
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:
......
{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, GADTs #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} -- don't want erroneous warning in test output
-- if removing this doesn't change output, then
-- remove it!
module T13337 where
import Data.Typeable
import Data.Kind
f :: forall k (a :: k). (Typeable k, Typeable a) => Proxy a -> Proxy Int
f p = case eqT :: Maybe (k :~: Type) of
Nothing -> Proxy
Just Refl -> case eqT :: Maybe (a :~: Int) of
Nothing -> Proxy
Just Refl -> p
......@@ -544,3 +544,4 @@ test('T12923', normal, compile, [''])
test('T12924', normal, compile, [''])
test('T12926', normal, compile, [''])
test('T13381', normal, compile_fail, [''])
test('T13337', normal, compile, [''])
Subproject commit 9acb2890cdb4369f3bb7fda899ff4d3526040e7d
Subproject commit 12a6cc9a98b79a4851fbe40a02c56652338d1c3e
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