# HG changeset patch
# User traytel
# Date 1317281879 -7200
# Node ID 7bb89635eb51c7ff4baf9d3e43c13175236da229
# Parent  6317e969fb30c2e0933e839730534c9eb1ddf368
correct coercion generation in case of unknown map functions

diff -r 6317e969fb30 -r 7bb89635eb51 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Sep 28 13:52:14 2011 +0200
+++ b/src/Tools/subtyping.ML	Thu Sep 29 09:37:59 2011 +0200
@@ -628,7 +628,7 @@
                 NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
                   " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
               | SOME (co, _) => co)
-      | ((Type (a, Ts)), (Type (b, Us))) =>
+      | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
             if a <> b
             then
               (case Symreltab.lookup (coes_of ctxt) (a, b) of
@@ -656,8 +656,11 @@
                   | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
               in
                 (case Symtab.lookup (tmaps_of ctxt) a of
-                  NONE => raise COERCION_GEN_ERROR
-                    (err ++> "No map function for " ^ quote a ^ " known")
+                  NONE =>
+                    if Type.could_unify (T1, T2)
+                    then Abs (Name.uu, T1, Bound 0)
+                    else raise COERCION_GEN_ERROR
+                      (err ++> "No map function for " ^ quote a ^ " known")
                 | SOME tmap =>
                     let
                       val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));