| WpApp Var -- [] d the 'd' is a type-class dictionary
| WpTyApp Type -- [] t the 't' is a type or corecion
- | WpLam Id -- \d. [] the 'd' is a type-class dictionary
- | WpTyLam TyVar -- \a. [] the 'a' is a type or coercion variable
+ | WpLam Var -- \d. [] the 'd' is a type-class dictionary or coercion variable
+ | WpTyLam TyVar -- \a. [] the 'a' is a type variable (not coercion var)
| WpInline -- inline_me [] Wrap inline around the thing
-- Non-empty bindings, so that the identity coercion
| ConPatOut {
pat_con :: Located DataCon,
- pat_tvs :: [TyVar], -- Existentially bound type variables
- -- including any bound coercion variables
- pat_dicts :: [id], -- Ditto dictionaries
+ pat_tvs :: [TyVar], -- Existentially bound type variables (tyvars only)
+ pat_dicts :: [id], -- Ditto *coercion variables* and *dictionaries*
+ -- One reason for putting coercion variable here, I think,
+ -- is to ensure their kinds are zonked
pat_binds :: DictBinds id, -- Bindings involving those dictionaries
pat_args :: HsConPatDetails id,
pat_ty :: Type -- The type of the pattern
; return (env2, WpCompose c1' c2') }
zonkCoFn env (WpCo co) = do { co' <- zonkTcTypeToType env co
; return (env, WpCo co') }
-zonkCoFn env (WpLam id) = do { id' <- zonkIdBndr env id
+zonkCoFn env (WpLam id) = do { id' <- zonkDictBndr env id
; let env1 = extendZonkEnv1 env id'
; return (env1, WpLam id') }
zonkCoFn env (WpTyLam tv) = ASSERT( isImmutableTyVar tv )
zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args })
= ASSERT( all isImmutableTyVar (pat_tvs p) )
do { new_ty <- zonkTcTypeToType env ty
- ; new_dicts <- zonkIdBndrs env dicts
+ ; new_dicts <- zonkDictBndrs env dicts
; let env1 = extendZonkEnv env new_dicts
; (env2, new_binds) <- zonkRecMonoBinds env1 binds
; (env', new_args) <- zonkConStuff env2 args
tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
-> TcType -- Type to instantiate
-> TcM ([TcTyVar], TcThetaType, TcType) -- Result
+ -- (type vars (excl coercion vars), preds (incl equalities), rho)
tcInstType inst_tyvars ty
= case tcSplitForAllTys ty of
([], rho) -> let -- There may be overloading despite no type variables;
-- it makes no difference
co = wrap_inline -- Note [Always inline implication constraints]
<.> mkWpTyLams tvs
- <.> mkWpTyLams eq_tyvars
+ <.> mkWpLams eq_tyvars
<.> mkWpLams dict_ids
<.> WpLet (binds `unionBags` bind)
wrap_inline | null dict_ids = idHsWrapper
}
tcGenericNormaliseFamInst fun (NoteTy note ty1)
= do { (coi,nty1) <- tcGenericNormaliseFamInst fun ty1
- ; return (mkNoteTyCoI note coi, NoteTy note nty1)
+ ; return (coi, NoteTy note nty1)
}
tcGenericNormaliseFamInst fun ty@(TyVarTy tv)
| isTcTyVar tv
split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split orig_ty (ForAllTy tv ty) ts
- | isCoVar tv = split ty ty (eq_pred:ts)
- where
- PredTy eq_pred = tyVarKind tv
+ | isCoVar tv = split ty ty (coVarPred tv : ts)
split orig_ty (FunTy arg res) ts
| Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
split orig_ty ty ts = (reverse ts, orig_ty)
-- list of "free vars" for the signature check.
; loc <- getInstLoc (SigOrigin skol_info)
- ; dicts <- newDictBndrs loc theta'
+ ; dicts <- newDictBndrs loc theta' -- Includes equalities
; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
; checkSigTyVarsWrt free_tvs tvs'
in (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
normaliseType env ty@(NoteTy note ty1)
= let (coi,nty1) = normaliseType env ty1
- in (mkNoteTyCoI note coi,NoteTy note nty1)
+ in (coi,NoteTy note nty1)
normaliseType env ty@(TyVarTy _)
= (IdCo,ty)
normaliseType env (PredTy predty)
argTypeKind, ubxTupleKind,
isLiftedTypeKindCon, isLiftedTypeKind,
mkArrowKind, mkArrowKinds, isCoercionKind,
+ coVarPred,
-- Kind constructors...
liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
isCoercionKind (NoteTy _ k) = isCoercionKind k
isCoercionKind (PredTy (EqPred {})) = True
isCoercionKind other = False
+
+coVarPred :: CoVar -> PredType
+coVarPred tv
+ = ASSERT( isCoVar tv )
+ case tyVarKind tv of
+ PredTy eq -> eq -- There shouldn't even be a NoteTy in the way
+ other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
\end{code}
ppr_type :: Prec -> Type -> SDoc
ppr_type p (TyVarTy tv) = ppr tv
ppr_type p (PredTy pred) = ifPprDebug (ptext SLIT("<pred>")) <> (ppr pred)
-ppr_type p (NoteTy other ty2) = ppr_type p ty2
+ppr_type p (NoteTy other ty2) = ifPprDebug (ptext SLIT("<note>")) <> ppr_type p ty2
ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
ppr_forall_type :: Prec -> Type -> SDoc
ppr_forall_type p ty
= maybeParen p FunPrec $
- sep [pprForAll tvs, pprThetaArrow (ctxt1 ++ ctxt2), pprType tau]
+ sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
where
- (tvs, ctxt1, rho) = split1 [] [] ty
- (ctxt2, tau) = split2 [] rho
+ (tvs, rho) = split1 [] ty
+ (ctxt, tau) = split2 [] rho
-- We need to be extra careful here as equality constraints will occur as
-- type variables with an equality kind. So, while collecting quantified
-- variables, we separate the coercion variables out and turn them into
-- equality predicates.
- split1 tvs eqs (ForAllTy tv ty)
- | isCoVar tv = split1 tvs (eq:eqs) ty
- | otherwise = split1 (tv:tvs) eqs ty
- where
- PredTy eq = tyVarKind tv
- split1 tvs eqs (NoteTy _ ty) = split1 tvs eqs ty
- split1 tvs eqs ty = (reverse tvs, reverse eqs, ty)
+ split1 tvs (ForAllTy tv ty)
+ | not (isCoVar tv) = split1 (tv:tvs) ty
+ split1 tvs (NoteTy _ ty) = split1 tvs ty
+ split1 tvs ty = (reverse tvs, ty)
split2 ps (NoteTy _ arg -- Rather a disgusting case
- `FunTy` res) = split2 ps (arg `FunTy` res)
- split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
- split2 ps (NoteTy _ ty) = split2 ps ty
- split2 ps ty = (reverse ps, ty)
+ `FunTy` res) = split2 ps (arg `FunTy` res)
+ split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
+ split2 ps (ForAllTy tv ty)
+ | isCoVar tv = split2 (coVarPred tv : ps) ty
+ split2 ps (NoteTy _ ty) = split2 ps ty
+ split2 ps ty = (reverse ps, ty)
ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
ppr_tc_app p tc []