-{- Simultaneous substitution on types for type variables,
- renaming as neceessary to avoid capture.
- No checks for correct kindedness. -}
-substl :: [Tvar] -> [Ty] -> Ty -> Ty
-substl tvs ts t = f (zip tvs ts) t
- where
- f env t0 =
- case t0 of
- Tcon _ -> t0
- Tvar v -> case lookup v env of
- Just t1 -> t1
- Nothing -> t0
- Tapp t1 t2 -> Tapp (f env t1) (f env t2)
- Tforall (t,k) t1 ->
- if t `elem` free then
- Tforall (t',k) (f ((t,Tvar t'):env) t1)
- else
- Tforall (t,k) (f (filter ((/=t).fst) env) t1)
- TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
- SymCoercion t1 -> SymCoercion (f env t1)
- UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
- LeftCoercion t1 -> LeftCoercion (f env t1)
- RightCoercion t1 -> RightCoercion (f env t1)
- InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
- where free = foldr union [] (map (freeTvars.snd) env)
- t' = freshTvar free
-
-{- Return free tvars in a type -}
-freeTvars :: Ty -> [Tvar]
-freeTvars (Tcon _) = []
-freeTvars (Tvar v) = [v]
-freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
-freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
-freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
-freeTvars (SymCoercion t) = freeTvars t
-freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
-freeTvars (LeftCoercion t) = freeTvars t
-freeTvars (RightCoercion t) = freeTvars t
-freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
-
-{- Return any tvar *not* in the argument list. -}
-freshTvar :: [Tvar] -> Tvar
-freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
-