60 fun mk_abs Ts t = Library.foldl (fn (u, T) => Abs ("", T, u)) (t, Ts); |
60 fun mk_abs Ts t = Library.foldl (fn (u, T) => Abs ("", T, u)) (t, Ts); |
61 |
61 |
62 fun unifyT sg env T U = |
62 fun unifyT sg env T U = |
63 let |
63 let |
64 val Envir.Envir {asol, iTs, maxidx} = env; |
64 val Envir.Envir {asol, iTs, maxidx} = env; |
65 val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U) |
65 val (iTs', maxidx') = Sign.typ_unify sg (T, U) (iTs, maxidx) |
66 in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end |
66 in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end |
67 handle Type.TUNIFY => error ("Non-unifiable types:\n" ^ |
67 handle Type.TUNIFY => error ("Non-unifiable types:\n" ^ |
68 Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U); |
68 Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U); |
69 |
69 |
70 fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) = |
70 fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) = |