| UnboundVariable of string
| WrongPred of string * pred * pred
-fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
- [PD.string s, PD.space 1, d]))
-
fun describe_unification_error t ue =
case ue of
UnifyPred (p1, p2) =>
TUnif (_, ref (SOME tAll)) => whnorm tAll
| _ => tAll
+fun baseCondition t =
+ case whnorm t of
+ (TBase name, _) => typeRule name
+ | (TList t, _) =>
+ (case baseCondition t of
+ NONE => NONE
+ | SOME f => SOME (fn (EList ls, _) => List.all f ls
+ | _ => false))
+ | _ => NONE
+
fun hasTyp (e, t1, t2) =
- case whnorm t2 of
- (TBase name, _) =>
- (case typeRule name of
- NONE => subTyp (t1, t2)
- | SOME rule =>
- if rule e then
- ()
- else
- subTyp (t1, t2))
- | _ => subTyp (t1, t2)
+ if (case baseCondition t2 of
+ NONE => false
+ | SOME rule => rule e) then
+ ()
+ else
+ subTyp (t1, t2)
fun checkTyp G (tAll as (t, loc)) =
let