Commit 565ef4cc authored by Simon Peyton Jones's avatar Simon Peyton Jones

Remove knot-tying bug in TcHsSyn.zonkTyVarOcc

There was a subtle knot-tying bug in TcHsSyn.zonkTyVarOcc, revealed
in Trac #15552.

I fixed it by

* Eliminating the short-circuiting optimisation in zonkTyVarOcc,
  instead adding a finite map to get sharing of zonked unification
  variables.

  See Note [Sharing when zonking to Type] in TcHsSyn

* On the way I /added/ the short-circuiting optimisation to
  TcMType.zonkTcTyVar, which has no such problem.  This turned
  out (based on non-systematic measurements) to be a modest win.

  See Note [Sharing in zonking] in TcMType

On the way I renamed some of the functions in TcHsSyn:

* Ones ending in "X" (like zonkTcTypeToTypeX) take a ZonkEnv

* Ones that do not end in "x" (like zonkTcTypeToType), don't.
  Instead they whiz up an empty ZonkEnv.
parent fda2ea58
......@@ -39,7 +39,7 @@ import Var
import TcRnMonad
import TcType
import TcMType
import TcHsSyn ( zonkTcTypeToType, mkEmptyZonkEnv, ZonkFlexi( RuntimeUnkFlexi ) )
import TcHsSyn ( zonkTcTypeToTypeX, mkEmptyZonkEnv, ZonkFlexi( RuntimeUnkFlexi ) )
import TcUnify
import TcEnv
......@@ -1258,7 +1258,8 @@ zonkTerm = foldTermM (TermFoldM
zonkRttiType :: TcType -> TcM Type
-- Zonk the type, replacing any unbound Meta tyvars
-- by RuntimeUnk skolems, safely out of Meta-tyvar-land
zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv RuntimeUnkFlexi)
zonkRttiType ty= do { ze <- mkEmptyZonkEnv RuntimeUnkFlexi
; zonkTcTypeToTypeX ze ty }
--------------------------------------------------------------------------------
-- Restore Class predicates out of a representation type
......
......@@ -73,7 +73,7 @@ tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type
tc_default_ty deflt_clss hs_ty
= do { (ty, _kind) <- solveEqualities $
tcLHsType hs_ty
; ty <- zonkTcTypeToType emptyZonkEnv ty -- establish Type invariants
; ty <- zonkTcTypeToType ty -- establish Type invariants
; checkValidType DefaultDeclCtxt ty
-- Check that the type is an instance of at least one of the deflt_clss
......
This diff is collapsed.
......@@ -253,8 +253,8 @@ tcHsDeriv hs_ty
; ty <- checkNoErrs $
-- avoid redundant error report with "illegal deriving", below
tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
; cls_kind <- zonkTcTypeToType emptyZonkEnv cls_kind
; ty <- zonkTcTypeToType emptyZonkEnv ty
; cls_kind <- zonkTcTypeToType cls_kind
; ty <- zonkTcTypeToType ty
; let (tvs, pred) = splitForAllTys ty
; let (args, _) = splitFunTys cls_kind
; case getClassPredTys_maybe pred of
......@@ -297,7 +297,7 @@ tcDerivStrategy user_ctxt mds thing_inside
cls_kind <- newMetaKindVar
ty' <- checkNoErrs $
tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) ty cls_kind
ty' <- zonkTcTypeToType emptyZonkEnv ty'
ty' <- zonkTcTypeToType ty'
let (via_tvs, via_pred) = splitForAllTys ty'
tcExtendTyVarEnv via_tvs $ do
(thing_tvs, thing) <- thing_inside
......@@ -322,7 +322,7 @@ tcHsClsInstType user_ctxt hs_inst_ty
types. Much better just to report the kind error directly. -}
do { inst_ty <- failIfEmitsConstraints $
tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
; inst_ty <- zonkTcTypeToType emptyZonkEnv inst_ty
; inst_ty <- zonkTcTypeToType inst_ty
; checkValidInstance user_ctxt hs_inst_ty inst_ty }
----------------------------------------------
......
......@@ -26,8 +26,7 @@ import TcClassDcl( tcClassDecl2, tcATDefault,
import TcSigs
import TcRnMonad
import TcValidity
import TcHsSyn ( zonkTyBndrsX, emptyZonkEnv
, zonkTcTypeToTypes, zonkTcTypeToType )
import TcHsSyn
import TcMType
import TcType
import BuildTyCl
......@@ -615,10 +614,10 @@ tcDataFamInstDecl mb_clsinfo
do { stupid_theta <- solveEqualities $ tcHsContext ctxt
-- Zonk the patterns etc into the Type world
; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
; pats' <- zonkTcTypeToTypes ze pats
; res_kind' <- zonkTcTypeToType ze res_kind
; stupid_theta' <- zonkTcTypeToTypes ze stupid_theta
; (ze, tvs') <- zonkTyBndrs tvs
; pats' <- zonkTcTypesToTypesX ze pats
; res_kind' <- zonkTcTypeToTypeX ze res_kind
; stupid_theta' <- zonkTcTypesToTypesX ze stupid_theta
; gadt_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta' cons
......
......@@ -72,7 +72,7 @@ module TcMType (
quantifyTyVars,
zonkTcTyCoVarBndr, zonkTcTyVarBinder,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
zonkTyCoVarKind,
zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
......@@ -1596,7 +1596,10 @@ zonkTcTyVar tv
-> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_kind_and_return
Indirect ty -> zonkTcType ty }
Indirect ty -> do { zty <- zonkTcType ty
; writeTcRef ref (Indirect zty)
-- See Note [Sharing in zonking]
; return zty } }
| otherwise -- coercion variable
= zonk_kind_and_return
......@@ -1622,7 +1625,26 @@ zonkTyVarTyVarPairs prs
do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
; return (nm, tv') }
{-
{- Note [Sharing in zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
alpha :-> beta :-> gamma :-> ty
where the ":->" means that the unification variable has been
filled in with Indirect. Then when zonking alpha, it'd be nice
to short-circuit beta too, so we end up with
alpha :-> zty
beta :-> zty
gamma :-> zty
where zty is the zonked version of ty. That way, if we come across
beta later, we'll have less work to do. (And indeed the same for
alpha.)
This is easily achieved: just overwrite (Indirect ty) with (Indirect
zty). Non-systematic perf comparisons suggest that this is a modest
win.
But c.f Note [Sharing when zonking to Type] in TcHsSyn.
%************************************************************************
%* *
Tidying
......
......@@ -23,8 +23,7 @@ import TcSigs( emptyPragEnv, completeSigFromId )
import TcType( mkMinimalBySCs )
import TcEnv
import TcMType
import TcHsSyn( zonkTyVarBindersX, zonkTcTypeToTypes
, zonkTcTypeToType, emptyZonkEnv )
import TcHsSyn
import TysPrim
import TysWiredIn ( runtimeRepTy )
import Name
......@@ -612,12 +611,12 @@ tc_patsyn_finish lname dir is_infix lpat'
= do { -- Zonk everything. We are about to build a final PatSyn
-- so there had better be no unification variables in there
(ze, univ_tvs') <- zonkTyVarBindersX emptyZonkEnv univ_tvs
; req_theta' <- zonkTcTypeToTypes ze req_theta
(ze, univ_tvs') <- zonkTyVarBinders univ_tvs
; req_theta' <- zonkTcTypesToTypesX ze req_theta
; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
; prov_theta' <- zonkTcTypeToTypes ze prov_theta
; pat_ty' <- zonkTcTypeToType ze pat_ty
; arg_tys' <- zonkTcTypeToTypes ze arg_tys
; prov_theta' <- zonkTcTypesToTypesX ze prov_theta
; pat_ty' <- zonkTcTypeToTypeX ze pat_ty
; arg_tys' <- zonkTcTypesToTypesX ze arg_tys
; let (env1, univ_tvs) = tidyTyVarBinders emptyTidyEnv univ_tvs'
(env2, ex_tvs) = tidyTyVarBinders env1 ex_tvs'
......
......@@ -2398,7 +2398,7 @@ tcRnType hsc_env normalise rdr_type
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kind <- zonkTcType kind
; kvs <- kindGeneralize kind
; ty <- zonkTcTypeToType emptyZonkEnv ty
; ty <- zonkTcTypeToType ty
; ty' <- if normalise
then do { fam_envs <- tcGetFamInstEnvs
......
......@@ -1183,7 +1183,7 @@ reifyInstances th_nm th_tys
<- failIfEmitsConstraints $ -- avoid error cascade if there are unsolved
tcImplicitTKBndrs ReifySkol tv_names $
fst <$> tcLHsType rn_ty
; ty <- zonkTcTypeToType emptyZonkEnv ty
; ty <- zonkTcTypeToType ty
-- Substitute out the meta type variables
-- In particular, the type might have kind
-- variables inside it (Trac #7477)
......
......@@ -552,8 +552,8 @@ kcTyClGroup decls
; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
; tc_res_kind' <- zonkTcTypeToType env tc_res_kind
; (env, all_binders') <- zonkTyVarBinders all_binders
; tc_res_kind' <- zonkTcTypeToTypeX env tc_res_kind
; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
-- See Note [Check telescope again during generalisation]
......@@ -1031,8 +1031,9 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
-- any unfilled coercion variables unless there is such an error
-- The zonk also squeeze out the TcTyCons, and converts
-- Skolems to tyvars.
; ctxt <- zonkTcTypeToTypes emptyZonkEnv ctxt
; sig_stuff <- mapM zonkTcMethInfoToMethInfo sig_stuff
; ze <- emptyZonkEnv
; ctxt <- zonkTcTypesToTypesX ze ctxt
; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff
-- ToDo: do we need to zonk at_stuff?
-- TODO: Allow us to distinguish between abstract class,
......@@ -1153,9 +1154,9 @@ tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = L _ tc_name
tcCheckLHsType rhs rhs_kind
-- Zonk the patterns etc into the Type world
; (ze, _) <- zonkTyBndrsX emptyZonkEnv tvs
; pats' <- zonkTcTypeToTypes ze pats
; rhs_ty' <- zonkTcTypeToType ze rhs_ty
; (ze, _) <- zonkTyBndrs tvs
; pats' <- zonkTcTypesToTypesX ze pats
; rhs_ty' <- zonkTcTypeToTypeX ze rhs_ty
; return (pats', rhs_ty') }
-- See Note [Type-checking default assoc decls]
......@@ -1345,7 +1346,7 @@ tcTySynRhs roles_info tc_name binders res_kind hs_ty
= do { env <- getLclEnv
; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; rhs_ty <- zonkTcTypeToType rhs_ty
; let roles = roles_info tc_name
tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
; return tycon }
......@@ -1369,8 +1370,7 @@ tcDataDefn roles_info
roles = roles_info tc_name
; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
stupid_tc_theta
; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta
; kind_signatures <- xoptM LangExt.KindSignatures
-- Check that we don't use kind signatures without Glasgow extensions
......@@ -1485,11 +1485,11 @@ tcTyFamInstEqn fam_tc mb_clsinfo
do { traceTc "tcTyFamInstEqn {" (ppr eqn_tc_name <+> ppr pats)
; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
; traceTc "tcTyFamInstEqn 1" (ppr eqn_tc_name <+> ppr pats)
; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
; (ze, tvs') <- zonkTyBndrs tvs
; traceTc "tcTyFamInstEqn 2" (ppr eqn_tc_name <+> ppr pats)
; pats' <- zonkTcTypeToTypes ze pats
; pats' <- zonkTcTypesToTypesX ze pats
; traceTc "tcTyFamInstEqn 3" (ppr eqn_tc_name <+> ppr pats $$ ppr rhs_ty)
; rhs_ty' <- zonkTcTypeToType ze rhs_ty
; rhs_ty' <- zonkTcTypeToTypeX ze rhs_ty
; traceTc "tcTyFamInstEqn 4" (ppr fam_tc <+> pprTyVars tvs')
; return (mkCoAxBranch tvs' [] pats' rhs_ty'
(map (const Nominal) tvs')
......@@ -1548,7 +1548,7 @@ kcDataDefn mb_kind_env
; let Pair lhs_ki rhs_ki = tcCoercionKind co
; when debugIsOn $
do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
do { (_, ev_binds) <- initZonkEnv zonkTcEvBinds ev_binds
; MASSERT( isEmptyTcEvBinds ev_binds )
; lhs_ki <- zonkTcType lhs_ki
; rhs_ki <- zonkTcType rhs_ki
......@@ -1933,10 +1933,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
-- any vars bound in exp_binders.
-- Zonk to Types
; (ze, qkvs) <- zonkTyBndrsX emptyZonkEnv kvs
; (ze, qkvs) <- zonkTyBndrs kvs
; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
; arg_tys <- zonkTcTypeToTypes ze arg_tys
; ctxt <- zonkTcTypeToTypes ze ctxt
; arg_tys <- zonkTcTypesToTypesX ze arg_tys
; ctxt <- zonkTcTypesToTypesX ze ctxt
; fam_envs <- tcGetFamInstEnvs
......@@ -2003,11 +2003,11 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
res_ty)
-- Zonk to Types
; (ze, tkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
; (ze, tkvs) <- zonkTyBndrs tkvs
; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
; arg_tys <- zonkTcTypeToTypes ze arg_tys
; ctxt <- zonkTcTypeToTypes ze ctxt
; res_ty <- zonkTcTypeToType ze res_ty
; arg_tys <- zonkTcTypesToTypesX ze arg_tys
; ctxt <- zonkTcTypesToTypesX ze ctxt
; res_ty <- zonkTcTypeToTypeX ze res_ty
; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
= rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
......
{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeInType, TypeFamilies #-}
module T15552 where
import Data.Kind
data Elem :: k -> [k] -> Type
data EntryOfVal (v :: Type) (kvs :: [Type]) where
EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type).
Elem (k, v) kvs -> EntryOfVal v kvs
type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type
type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs
type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where
{-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeInType, TypeFamilies #-}
{- # LANGUAGE UndecidableInstances #-}
module T15552 where
import Data.Kind
data Elem :: k -> [k] -> Type where
Here :: Elem x (x : xs)
There :: Elem x xs -> Elem x (y : xs)
data EntryOfVal (v :: Type) (kvs :: [Type]) where
EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type).
Elem (k, v) kvs -> EntryOfVal v kvs
type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type where
EntryOfValKey ('EntryOfVal (_ :: Elem (k, v) kvs)) = k
type family GetEntryOfVal (eov :: EntryOfVal v kvs)
:: Elem (EntryOfValKey eov, v) kvs
where
GetEntryOfVal ('EntryOfVal e) = e
type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs
where FirstEntryOfVal v (_ : kvs)
= 'EntryOfVal (There (GetEntryOfVal (FirstEntryOfVal v kvs)))
--type instance FirstEntryOfVal v (_ : kvs)
-- = 'EntryOfVal ('There (GetEntryOfVal (FirstEntryOfVal v kvs)))
T15552a.hs:25:9: error:
• Illegal nested type family application ‘EntryOfValKey
(FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
T15552a.hs:25:9: error:
• Illegal nested type family application ‘EntryOfValKey
(FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
T15552a.hs:25:9: error:
• Illegal nested type family application ‘GetEntryOfVal
(FirstEntryOfVal v kvs)’
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘FirstEntryOfVal’
In the type family declaration for ‘FirstEntryOfVal’
......@@ -479,3 +479,5 @@ test('T15361', normal, compile_fail, [''])
test('T15438', normal, compile_fail, [''])
test('T15523', normal, compile_fail, ['-O'])
test('T15527', normal, compile_fail, [''])
test('T15552', normal, compile, [''])
test('T15552a', normal, compile_fail, [''])
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