do not try to support subtyping between a restriction type & non-rest…

…riction type
RedPRL · Aug 14, 2018 · f4df7db · f4df7db
1 parent 18a56fb
commit f4df7db
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 11 deletions.
diff --git a/src/core/Quote.ml b/src/core/Quote.ml
@@ -749,15 +749,9 @@ struct
 
   and fancy_subtype env ty0 sys0 ty1 sys1 =
     match unleash ty0, unleash ty1 with
-    | _, Rst rst1 ->
-      fancy_subtype env ty0 sys0 rst1.ty (rst1.sys @ sys1)
-
-    | Rst rst0, _ ->
+    | Rst rst0, Rst rst1 ->
       begin
-        (* backtracking :( ) *)
-        try fancy_subtype env rst0.ty sys0 ty1 sys1
-        with _ ->
-          fancy_subtype env rst0.ty (rst0.sys @ sys0) ty1 sys1
+        fancy_subtype env rst0.ty (rst0.sys @ sys0) ty1 (rst1.sys @ sys1)
       end
 
     | Pi pi0, Pi pi1 ->

diff --git a/src/frontend/Unify.ml b/src/frontend/Unify.ml
@@ -639,9 +639,6 @@ let rec subtype ty0 ty1 =
     | Tm.Rst rst0, Tm.Rst rst1 ->
       restriction_subtype rst0.ty rst0.sys rst1.ty rst1.sys
 
-    | Tm.Rst _, _ ->
-      active @@ Subtype {ty0; ty1 = Tm.make @@ Tm.Rst {ty = ty1; sys = []}}
-
     | _ ->
       active @@ Problem.eqn ~ty0:univ ~ty1:univ ~tm0:ty0 ~tm1:ty1