Added some tricky transfer type checking examples.

transfer/examples/tricky-type-checking.tra

@@ -0,0 +1,31 @@
+
+--
+-- Pattern matching and inductive families.
+--
+
+data Tree : Type -> Type where
+  EAdd : Tree Integer -> Tree Integer -> Tree Integer
+  EInt : Integer -> Tree Integer
+  EFoo : (A:Type) -> A -> Tree A
+
+strip : (B : Type) -> Tree B -> B
+strip _ t = case t of
+		EAdd x y -> x+y
+		EInt i -> i
+		EFoo _ x -> x
+
+--
+-- Subtyping
+--
+
+getX : { x : Integer } -> Integer
+getX r = r.x
+
+getY : { y : Integer } -> Integer
+getY r = r.y
+
+proj2 : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B) -> (A -> C) -> A -> (B,C)
+proj2 _ _ _ f g x = (f x, g x)
+
+getXY : { x : Integer, y : Integer } -> (Integer,Integer)
+getXY r = proj2 ? ? ? getX getY r