-\begin{code}
-boxyMatchTypes
- :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
- -> [BoxySigmaType] -- Type to match
- -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
-
--- boxyMatchTypes implements the Pre-matching judgement, in Fig 5 of the paper
--- "Boxy types: inference for higher rank types and impredicativity"
-
--- Find a *boxy* substitution that makes the template look as much
--- like the BoxySigmaType as possible.
--- It's always ok to return an empty substitution;
--- anything more is jam on the pudding
---
--- NB1: This is a pure, non-monadic function.
--- It does no unification, and cannot fail
---
--- Precondition: the arg lengths are equal
--- Precondition: none of the template type variables appear anywhere in the [BoxySigmaType]
---
-
-------------
-boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
- = ASSERT( length tmpl_tys == length boxy_tys )
- boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
- -- ToDo: add error context?
-
-boxy_match_s tmpl_tvs [] boxy_tvs [] subst
- = subst
-boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
- = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
- boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
-boxy_match_s tmpl_tvs _ boxy_tvs _ subst
- = panic "boxy_match_s" -- Lengths do not match
-
-
-------------
-boxy_match :: TcTyVarSet -> TcType -- Template
- -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these
- -> BoxySigmaType -- Match against this type
- -> TvSubst
- -> TvSubst
-
--- The boxy_tvs argument prevents this match:
--- [a] forall b. a ~ forall b. b
--- We don't want to bind the template variable 'a'
--- to the quantified type variable 'b'!
-
-boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
- = go orig_tmpl_ty orig_boxy_ty
- where
- go t_ty b_ty
- | Just t_ty' <- tcView t_ty = go t_ty' b_ty
- | Just b_ty' <- tcView b_ty = go t_ty b_ty'
-
- go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType
- | isSigmaTy ty1
- , (tvs1, _, tau1) <- tcSplitSigmaTy ty1
- , (tvs2, _, tau2) <- tcSplitSigmaTy ty2
- , equalLength tvs1 tvs2
- = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1
- (boxy_tvs `extendVarSetList` tvs2) tau2 subst
-
- go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
- | tc1 == tc2 = go_s tys1 tys2
-
- go (FunTy arg1 res1) (FunTy arg2 res2)
- = go_s [arg1,res1] [arg2,res2]
-
- go t_ty b_ty
- | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
- Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
- typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant
- = go_s [s1,t1] [s2,t2]
-
- go (TyVarTy tv) b_ty
- | tv `elemVarSet` tmpl_tvs -- Template type variable in the template
- , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty
- , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds]
- = extendTvSubst subst tv boxy_ty'
- | otherwise
- = subst -- Ignore others
- where
- boxy_ty' = case lookupTyVar subst tv of
- Nothing -> orig_boxy_ty
- Just ty -> ty `boxyLub` orig_boxy_ty
-
- go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution
- -- Example: Tree a ~ Maybe Int
- -- We do not want to bind (a |-> Int) in pre-matching, because that can give very
- -- misleading error messages. An even more confusing case is
- -- a -> b ~ Maybe Int
- -- Then we do not want to bind (b |-> Int)! It's always safe to discard bindings
- -- from this pre-matching phase.
-
- --------
- go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
-
-
-boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
--- Combine boxy information from the two types
--- If there is a conflict, return the first
-boxyLub orig_ty1 orig_ty2
- = go orig_ty1 orig_ty2
- where
- go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
- go (FunTy f1 a1) (FunTy f2 a2) = FunTy (boxyLub f1 f2) (boxyLub a1 a2)
- go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
- | tc1 == tc2, length ts1 == length ts2
- = TyConApp tc1 (zipWith boxyLub ts1 ts2)
-
- go (TyVarTy tv1) ty2 -- This is the whole point;
- | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
- = orig_ty2
-
- -- Look inside type synonyms, but only if the naive version fails
- go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
- | Just ty2' <- tcView ty1 = go ty1 ty2'
-
- -- For now, we don't look inside ForAlls, PredTys
- go ty1 ty2 = orig_ty1 -- Default