Do a lot more type simplification for error messages

4 files changed, 192 insertions, 16 deletions

diff --git a/src/elab_err.sml b/src/elab_err.sml
index 2bf059e6..1951d971 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -36,20 +36,6 @@ structure U = ElabUtil
 open Print
 structure P = ElabPrint
 
-val simplCon = U.Con.mapB {kind = fn _ => fn k => k,
-                           con = fn env => fn c =>
-                                              let
-                                                  val c = (c, ErrorMsg.dummySpan)
-                                                  val c' = ElabOps.hnormCon env c
-                                              in
-                                                  (*prefaces "simpl" [("c", P.p_con env c),
-                                                                    ("c'", P.p_con env c')];*)
-                                                  #1 c'
-                                              end,
-                           bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k
-                                   | (env, U.Con.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
-                                   | (env, _) => env}
-
 val p_kind = P.p_kind
              
 datatype kind_error =
@@ -80,7 +66,7 @@ fun kunifyError env err =
         [("Kind 1", p_kind env k1),
          ("Kind 2", p_kind env k2)]
 
-fun p_con env c = P.p_con env (simplCon env c)
+fun p_con env c = P.p_con env (ElabOps.reduceCon env c)
 
 datatype con_error =
          UnboundCon of ErrorMsg.span * string
@@ -195,7 +181,14 @@ datatype exp_error =
      | OutOfContext of ErrorMsg.span * (exp * con) option
      | IllegalRec of string * exp
 
-val p_exp = P.p_exp
+val simplExp = U.Exp.mapB {kind = fn _ => fn k => k,
+                           con = fn env => fn c => #1 (ElabOps.reduceCon env (c, ErrorMsg.dummySpan)),
+                           exp = fn _ => fn e => e,
+                           bind = fn (env, U.Exp.RelC (x, k)) => E.pushCRel env x k
+                                   | (env, U.Exp.NamedC (x, n, k, co)) => E.pushCNamedAs env x n k co
+                                   | (env, _) => env}
+
+fun p_exp env e = P.p_exp env (simplExp env e)
 val p_pat = P.p_pat
 
 fun expError env err =
diff --git a/src/elab_ops.sig b/src/elab_ops.sig
index ed4c7d68..97e4b602 100644
--- a/src/elab_ops.sig
+++ b/src/elab_ops.sig
@@ -40,6 +40,7 @@ signature ELAB_OPS = sig
     val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn
 
     val hnormCon : ElabEnv.env -> Elab.con -> Elab.con
+    val reduceCon : ElabEnv.env -> Elab.con -> Elab.con
 
     val identity : int ref
     val distribute : int ref
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index dc9f69a4..dbefbe7d 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -324,4 +324,179 @@ fun hnormCon env (cAll as (c, loc)) =
 
       | _ => cAll
 
+fun reduceCon env (cAll as (c, loc)) =
+    case c of
+        TFun (c1, c2) => (TFun (reduceCon env c1, reduceCon env c2), loc)
+      | TCFun (exp, x, k, c) => (TCFun (exp, x, k, reduceCon env c), loc)
+      | TRecord c => (TRecord (reduceCon env c), loc)
+      | TDisjoint (c1, c2, c3) => (TDisjoint (reduceCon env c1, reduceCon env c2, reduceCon env c3), loc)
+
+      | CRel _ => cAll
+      | CNamed xn =>
+        (case E.lookupCNamed env xn of
+             (_, _, SOME c') => reduceCon env c'
+           | _ => cAll)
+      | CModProj _ => cAll
+      | CApp (c1, c2) =>
+        let
+            val c1 = reduceCon env c1
+            val c2 = reduceCon env c2
+            fun default () = (CApp (c1, c2), loc)
+        in
+            case #1 c1 of
+                CAbs (x, k, cb) =>
+                ((reduceCon env (subConInCon (0, c2) cb))
+                 handle SynUnif => default ())
+              | CApp (c', f) =>
+                let
+                    val c' = reduceCon env c'
+                    val f = reduceCon env f
+                in
+                    case #1 c' of
+                        CMap (ks as (k1, k2)) =>
+                        (case #1 c2 of
+                             CRecord (_, []) => (CRecord (k2, []), loc)
+                           | CRecord (_, (x, c) :: rest) =>
+                             reduceCon env
+                                       (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                                 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
+                           | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+                             let
+                                 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+                             in
+                                 reduceCon env
+                                           (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
+                                                     (CApp (c1, rest''), loc)), loc)
+                             end
+                           | _ =>
+                             let
+                                 fun unconstraint c =
+                                     case reduceCon env c of
+                                         (TDisjoint (_, _, c), _) => unconstraint c
+                                       | c => c
+
+                                 fun inc r = r := !r + 1
+
+                                 fun tryDistributivity () =
+                                     case reduceCon env c2 of
+                                         (CConcat (c1, c2), _) =>
+                                         let
+                                             val c = (CMap ks, loc)
+                                             val c = (CApp (c, f), loc)
+                                                  
+                                             val c1 = (CApp (c, c1), loc)
+                                             val c2 = (CApp (c, c2), loc)
+                                             val c = (CConcat (c1, c2), loc)
+                                         in
+                                             inc distribute;
+                                             reduceCon env c
+                                         end
+                                       | _ => default ()
+
+                                 fun tryFusion () =
+                                     case #1 (reduceCon env c2) of
+                                         CApp (f', r') =>
+                                         (case #1 (reduceCon env f') of
+                                              CApp (f', inner_f) =>
+                                              (case #1 (reduceCon env f') of
+                                                   CMap (dom, _) =>
+                                                   let
+                                                       val inner_f = liftConInCon 0 inner_f
+                                                       val f = liftConInCon 0 f
+
+                                                       val f' = (CApp (inner_f, (CRel 0, loc)), loc)
+                                                       val f' = (CApp (f, f'), loc)
+                                                       val f' = (CAbs ("v", dom, f'), loc)
+
+                                                       val c = (CMap (dom, k2), loc)
+                                                       val c = (CApp (c, f'), loc)
+                                                       val c = (CApp (c, r'), loc)
+                                                   in
+                                                       inc fuse;
+                                                       reduceCon env c
+                                                   end
+                                                 | _ => tryDistributivity ())
+                                            | _ => tryDistributivity ())
+                                       | _ => tryDistributivity ()
+
+                                 fun tryIdentity () =
+                                     let
+                                         fun cunif () =
+                                             let
+                                                 val r = ref (Unknown (fn _ => true))
+                                             in
+                                                 (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
+                                             end
+                                             
+                                         val (vR, v) = cunif ()
+
+                                         val c = (CApp (f, v), loc)
+                                     in
+                                         case unconstraint c of
+                                             (CUnif (_, _, _, _, vR'), _) =>
+                                             if vR' = vR then
+                                                 (inc identity;
+                                                  reduceCon env c2)
+                                             else
+                                                 tryFusion ()
+                                           | _ => tryFusion ()
+                                     end
+                             in
+                                 tryIdentity ()
+                             end)
+                      | _ => default ()
+                end
+              | _ => default ()
+        end
+      | CAbs (x, k, b) =>
+        let
+            val b = reduceCon (E.pushCRel env x k) b
+            fun default () = (CAbs (x, k, b), loc)
+        in
+            case #1 b of
+                CApp (f, (CRel 0, _)) =>
+                if occurs f then
+                    default ()
+                else
+                    reduceCon env (subConInCon (0, (CUnit, loc)) f)
+              | _ => default ()
+        end
+
+      | CKAbs (x, b) => (CKAbs (x, reduceCon (E.pushKRel env x) b), loc)
+      | CKApp (c1, k) =>
+        (case reduceCon env c1 of
+             (CKAbs (_, body), _) => reduceCon env (subKindInCon (0, k) body)
+           | c1 => (CKApp (c1, k), loc))
+      | TKFun (x, c) => (TKFun (x, reduceCon env c), loc)
+
+      | CName _ => cAll
+
+      | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (reduceCon env x, reduceCon env c)) xcs), loc)
+      | CConcat (c1, c2) =>
+        let
+            val c1 = reduceCon env c1
+            val c2 = reduceCon env c2
+        in
+            case (c1, c2) of
+                ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => (CRecord (k, xcs1 @ xcs2), loc)
+              | ((CRecord (_, []), _), _) => c2
+              | ((CConcat (c11, c12), loc), _) => reduceCon env (CConcat (c11, (CConcat (c12, c2), loc)), loc)
+              | (_, (CRecord (_, []), _)) => c1
+              | _ => (CConcat (c1, c2), loc)
+        end
+      | CMap _ => cAll
+
+      | CUnit => cAll
+
+      | CTuple cs => (CTuple (map (reduceCon env) cs), loc)
+      | CProj (c, n) =>
+        (case reduceCon env c of
+             (CTuple cs, _) => reduceCon env (List.nth (cs, n - 1))
+           | c => (CProj (c, n), loc))
+
+      | CError => cAll
+
+      | CUnif (nl, _, _, _, ref (Known c)) => reduceCon env (E.mliftConInCon nl c)
+      | CUnif _ => cAll
+
 end
diff --git a/tests/league.ur b/tests/league.ur
new file mode 100644
index 00000000..7edd5f42
--- /dev/null
+++ b/tests/league.ur
@@ -0,0 +1,7 @@
+type team = string
+type league = string
+
+table team : { Id : team,
+               League : league }
+
+val foo:int = queryL(SELECT * FROM team)