2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 %************************************************************************
8 Type refinement for GADTs
10 %************************************************************************
14 Refinement, emptyRefinement, isEmptyRefinement,
16 refineType, refinePred, refineResType,
17 tcUnifyTys, BindFlag(..)
20 #include "HsVersions.h"
40 %************************************************************************
44 %************************************************************************
47 data Refinement = Reft InScopeSet InternalReft
49 type InternalReft = TyVarEnv (Coercion, Type)
50 -- INVARIANT: a->(co,ty) then co :: (a:=:ty)
51 -- Not necessarily idemopotent
53 instance Outputable Refinement where
54 ppr (Reft _in_scope env)
55 = ptext SLIT("Refinement") <+>
58 emptyRefinement :: Refinement
59 emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
61 isEmptyRefinement :: Refinement -> Bool
62 isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
64 refineType :: Refinement -> Type -> Maybe (Coercion, Type)
65 -- Apply the refinement to the type.
66 -- If (refineType r ty) = (co, ty')
67 -- Then co :: ty:=:ty'
68 -- Nothing => the refinement does nothing to this type
69 refineType (Reft in_scope env) ty
70 | not (isEmptyVarEnv env), -- Common case
71 any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
72 = Just (substTy co_subst ty, substTy tv_subst ty)
74 = Nothing -- The type doesn't mention any refined type variables
76 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
77 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
79 refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
80 refinePred (Reft in_scope env) pred
81 | not (isEmptyVarEnv env), -- Common case
82 any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
83 = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
85 = Nothing -- The type doesn't mention any refined type variables
87 tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
88 co_subst = mkTvSubst in_scope (mapVarEnv fst env)
90 refineResType :: Refinement -> Type -> (HsWrapper, Type)
91 -- Like refineType, but returns the 'sym' coercion
92 -- If (refineResType r ty) = (co, ty')
93 -- Then co :: ty':=:ty
94 -- It's convenient to return a HsWrapper here
96 = case refineType reft ty of
97 Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1)
98 Nothing -> (idHsWrapper, ty)
102 %************************************************************************
104 Simple generation of a type refinement
106 %************************************************************************
109 matchRefine :: [CoVar] -> Refinement
112 Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2
113 is a specialisation of ty1, produce a type refinement that maps the variables
114 of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg,
116 matchRefine (co :: [(a, b)] ~ [(c, Maybe d)])
117 = { right (left (right co)) :: a ~ c
118 , right (right co) :: b ~ Maybe d
121 Precondition: The rhs types must indeed be a specialisation of the lhs types;
122 i.e., some free variables of the lhs are replaced with either distinct free
123 variables or proper type terms to obtain the rhs. (We don't perform full
124 unification or type matching here!)
126 NB: matchRefine does *not* expand the type synonyms.
130 = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars))
132 in_scope = foldr extend emptyInScopeSet co_vars
134 -- For each co_var, add it *and* the tyvars it mentions, to in_scope
135 extend co_var in_scope
136 = extendInScopeSetSet in_scope $
137 extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
139 refineOne co_var = refine (TyVarTy co_var) ty1 ty2
141 (ty1, ty2) = splitCoercionKind (tyVarKind co_var)
143 refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty)
144 refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys'
145 refine co (NoteTy _ ty) ty' = refine co ty ty'
146 refine co ty (NoteTy _ ty') = refine co ty ty'
147 refine _ (PredTy _) (PredTy _) =
148 error "TcGadt.matchRefine: PredTy"
149 refine co (FunTy arg res) (FunTy arg' res') =
150 refine (mkRightCoercion (mkLeftCoercion co)) arg arg'
152 refine (mkRightCoercion co) res res'
153 refine co (AppTy fun arg) (AppTy fun' arg') =
154 refine (mkLeftCoercion co) fun fun'
156 refine (mkRightCoercion co) arg arg'
157 refine co (ForAllTy tv ty) (ForAllTy _tv ty') =
158 refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv
159 refine _ _ _ = error "RcGadt.matchRefine: mismatch"
161 refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft
162 refineArgs co tys tys' =
163 fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys')
165 refineArg (ty, ty') (reft, coWrapper)
166 = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft,
167 mkLeftCoercion . coWrapper)
171 %************************************************************************
175 %************************************************************************
178 tcUnifyTys :: (TyVar -> BindFlag)
180 -> Maybe TvSubst -- A regular one-shot substitution
181 -- The two types may have common type variables, and indeed do so in the
182 -- second call to tcUnifyTys in FunDeps.checkClsFD
184 -- We implement tcUnifyTys using the evidence-generating 'unify' function
185 -- in this module, even though we don't need to generate any evidence.
186 -- This is simply to avoid replicating all all the code for unify
187 tcUnifyTys bind_fn tys1 tys2
188 = maybeErrToMaybe $ initUM bind_fn $
189 do { reft <- unifyList emptyInternalReft cos tys1 tys2
191 -- Find the fixed point of the resulting non-idempotent substitution
192 ; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
193 tv_env = fixTvSubstEnv in_scope (mapVarEnv snd reft)
195 ; return (mkTvSubst in_scope tv_env) }
197 tvs1 = tyVarsOfTypes tys1
198 tvs2 = tyVarsOfTypes tys2
199 cos = zipWith mkUnsafeCoercion tys1 tys2
202 ----------------------------
203 -- XXX Can we do this more nicely, by exploiting laziness?
204 -- Or avoid needing it in the first place?
205 fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
206 fixTvSubstEnv in_scope env = f env
208 f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e
209 in if and $ eltsUFM $ intersectUFM_C tcEqType e e'
216 %************************************************************************
220 %************************************************************************
223 emptyInternalReft :: InternalReft
224 emptyInternalReft = emptyVarEnv
226 unify :: InternalReft -- An existing substitution to extend
227 -> Coercion -- Witness of their equality
228 -> Type -> Type -- Types to be unified, and witness of their equality
229 -> UM InternalReft -- Just the extended substitution,
230 -- Nothing if unification failed
231 -- We do not require the incoming substitution to be idempotent,
232 -- nor guarantee that the outgoing one is. That's fixed up by
235 -- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
238 -- Respects newtypes, PredTypes
240 unify subst co ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
241 unify_ subst co ty1 ty2
243 -- in unify_, any NewTcApps/Preds should be taken at face value
244 unify_ subst co (TyVarTy tv1) ty2 = uVar False subst co tv1 ty2
245 unify_ subst co ty1 (TyVarTy tv2) = uVar True subst co tv2 ty1
247 unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
248 unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'
250 unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2
252 unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2)
253 | tyc1 == tyc2 = unify_tys subst co tys1 tys2
255 unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b)
256 = do { let [co1,co2] = decomposeCo 2 co
257 ; subst' <- unify subst co1 ty1a ty2a
258 ; unify subst' co2 ty1b ty2b }
260 -- Applications need a bit of care!
261 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
262 -- NB: we've already dealt with type variables and Notes,
263 -- so if one type is an App the other one jolly well better be too
264 unify_ subst co (AppTy ty1a ty1b) ty2
265 | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
266 = do { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
267 ; unify subst' (mkRightCoercion co) ty1b ty2b }
269 unify_ subst co ty1 (AppTy ty2a ty2b)
270 | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
271 = do { subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
272 ; unify subst' (mkRightCoercion co) ty1b ty2b }
274 unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
278 ------------------------------
279 unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
280 | c1 == c2 = unify_tys subst co tys1 tys2
281 unify_pred subst co (IParam n1 t1) (IParam n2 t2)
282 | n1 == n2 = unify subst co t1 t2
283 unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
285 ------------------------------
286 unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
287 unify_tys subst co xs ys
288 = unifyList subst (decomposeCo (length xs) co) xs ys
290 unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
291 unifyList subst orig_cos orig_xs orig_ys
292 = go subst orig_cos orig_xs orig_ys
294 go subst _ [] [] = return subst
295 go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
296 ; go subst' cos xs ys }
297 go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)
299 ---------------------------------
300 uVar :: Bool -- Swapped
301 -> InternalReft -- An existing substitution to extend
303 -> TyVar -- Type variable to be unified
304 -> Type -- with this type
307 -- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
308 -- if swap=False co :: (tv1:=:ty)
309 -- if swap=True co :: (ty:=:tv1)
311 uVar swap subst co tv1 ty
312 = -- Check to see whether tv1 is refined by the substitution
313 case (lookupVarEnv subst tv1) of
315 -- Yes, call back into unify'
316 Just (co',ty') -- co' :: (tv1:=:ty')
317 | swap -- co :: (ty:=:tv1)
318 -> unify subst (mkTransCoercion co co') ty ty'
319 | otherwise -- co :: (tv1:=:ty)
320 -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty
323 Nothing -> uUnrefined swap subst co
327 uUnrefined :: Bool -- Whether the input is swapped
328 -> InternalReft -- An existing substitution to extend
330 -> TyVar -- Type variable to be unified
331 -> Type -- with this type
332 -> Type -- (de-noted version)
335 -- We know that tv1 isn't refined
336 -- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that
338 -- and if the first argument is True instead, we know
341 uUnrefined swap subst co tv1 ty2 ty2'
342 | Just ty2'' <- tcView ty2'
343 = uUnrefined swap subst co tv1 ty2 ty2'' -- Unwrap synonyms
344 -- This is essential, in case we have
346 -- and then unify a :=: Foo a
348 uUnrefined swap subst co tv1 ty2 (TyVarTy tv2)
349 | tv1 == tv2 -- Same type variable
352 -- Check to see whether tv2 is refined
353 | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty'
354 = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty'
356 -- So both are unrefined; next, see if the kinds force the direction
357 | eqKind k1 k2 -- Can update either; so check the bind-flags
358 = do { b1 <- tvBindFlag tv1
359 ; b2 <- tvBindFlag tv2
361 (BindMe, _) -> bind swap tv1 ty2
363 (AvoidMe, BindMe) -> bind (not swap) tv2 ty1
364 (AvoidMe, _) -> bind swap tv1 ty2
366 (WildCard, WildCard) -> return subst
367 (WildCard, Skolem) -> return subst
368 (WildCard, _) -> bind (not swap) tv2 ty1
370 (Skolem, WildCard) -> return subst
371 (Skolem, Skolem) -> failWith (misMatch ty1 ty2)
372 (Skolem, _) -> bind (not swap) tv2 ty1
375 | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1 -- Must update tv2
376 | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2 -- Must update tv1
378 | otherwise = failWith (kindMisMatch tv1 ty2)
383 bind swap tv ty = extendReft swap subst tv co ty
385 uUnrefined swap subst co tv1 ty2 ty2' -- ty2 is not a type variable
386 | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
387 = failWith (occursCheck tv1 ty2) -- Occurs check
388 | not (k2 `isSubKind` k1)
389 = failWith (kindMisMatch tv1 ty2) -- Kind check
391 = bindTv swap subst co tv1 ty2 -- Bind tyvar to the synonym if poss
396 substTvSet :: InternalReft -> TyVarSet -> TyVarSet
397 -- Apply the non-idempotent substitution to a set of type variables,
398 -- remembering that the substitution isn't necessarily idempotent
400 = foldVarSet (unionVarSet . get) emptyVarSet tvs
402 get tv = case lookupVarEnv subst tv of
403 Nothing -> unitVarSet tv
404 Just (_,ty) -> substTvSet subst (tyVarsOfType ty)
406 bindTv swap subst co tv ty -- ty is not a type variable
407 = do { b <- tvBindFlag tv
409 Skolem -> failWith (misMatch (TyVarTy tv) ty)
410 WildCard -> return subst
411 other -> extendReft swap subst tv co ty
414 doSwap :: Bool -> Coercion -> Coercion
415 doSwap swap co = if swap then mkSymCoercion co else co
423 extendReft swap subst tv co ty
424 = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty),
425 (text "Refinement invariant failure: co = " <+> ppr co1 <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
426 return (extendVarEnv subst tv (co1, ty))
432 %************************************************************************
436 %************************************************************************
440 = BindMe -- A regular type variable
441 | AvoidMe -- Like BindMe but, given the choice, avoid binding it
443 | Skolem -- This type variable is a skolem constant
444 -- Don't bind it; it only matches itself
446 | WildCard -- This type variable matches anything,
447 -- and does not affect the substitution
449 newtype UM a = UM { unUM :: (TyVar -> BindFlag)
450 -> MaybeErr Message a }
452 instance Monad UM where
453 return a = UM (\tvs -> Succeeded a)
454 fail s = UM (\tvs -> Failed (text s))
455 m >>= k = UM (\tvs -> case unUM m tvs of
456 Failed err -> Failed err
457 Succeeded v -> unUM (k v) tvs)
459 initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
460 initUM badtvs um = unUM um badtvs
462 tvBindFlag :: TyVar -> UM BindFlag
463 tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))
465 failWith :: Message -> UM a
466 failWith msg = UM (\tv_fn -> Failed msg)
468 maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
469 maybeErrToMaybe (Succeeded a) = Just a
470 maybeErrToMaybe (Failed m) = Nothing
474 %************************************************************************
477 We go to a lot more trouble to tidy the types
478 in TcUnify. Maybe we'll end up having to do that
479 here too, but I'll leave it for now.
481 %************************************************************************
485 = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+>
486 ptext SLIT("and") <+> quotes (ppr t2)
488 lengthMisMatch tys1 tys2
489 = sep [ptext SLIT("Can't match unequal length lists"),
490 nest 2 (ppr tys1), nest 2 (ppr tys2) ]
493 = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+>
494 ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
495 ptext SLIT("when matching") <+> quotes (ppr tv1) <+>
496 ptext SLIT("with") <+> quotes (ppr t2)]
499 = hang (ptext SLIT("Can't construct the infinite type"))
500 2 (ppr tv <+> equals <+> ppr ty)