diff tests/type_class.ur @ 677:81573f62d6c3

Enforce termination of type class instances
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 15:54:04 -0400
parents 43430b7190f4
children
line wrap: on
line diff
--- a/tests/type_class.ur	Thu Mar 26 15:26:35 2009 -0400
+++ b/tests/type_class.ur	Thu Mar 26 15:54:04 2009 -0400
@@ -10,10 +10,16 @@
     val option_default : t ::: Type -> default t -> default (option t)
     val pair_default : a ::: Type -> b ::: Type -> default a -> default b -> default (pair a b)
 
+    (*val uh_oh : t ::: Type -> default t -> default t*)
+
     class awesome
     val awesome_default : t ::: Type -> awesome t -> default t
 
     val float_awesome : awesome float
+
+    val oh_my : t ::: Type -> awesome (option t) -> awesome (option t)
+
+    val awesome : t ::: Type -> awesome t -> t
 end = struct
     class default t = t
     fun get (t ::: Type) (x : t) = x
@@ -24,10 +30,16 @@
     fun option_default (t ::: Type) (x : t) = Some x
     fun pair_default (a ::: Type) (b ::: Type) (x : a) (y : b) = Pair (x, y)
 
+    (*fun uh_oh (t ::: Type) (x : t) = x*)
+
     class awesome t = t
     fun awesome_default (t ::: Type) (x : t) = x
 
     val float_awesome = 1.23
+
+    fun oh_my (t ::: Type) (x : option t) = x
+
+    fun awesome (t ::: Type) (x : t) = x
 end
 
 open M
@@ -49,6 +61,8 @@
                    None => "None"
                  | Some y => show y)
 
+(*val x : option float = awesome*)
+
 fun show_pair (a ::: Type) (b ::: Type) (_ : show a) (_ : show b) : show (pair a b) =
     mkShow (fn x =>
                case x of