diff --git a/.gitignore b/.gitignore
index 5cf744d27..a8b992ff8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -109,4 +109,6 @@ selfhost/.js
 selfhost/main.js
 selfhost/tests/*.wyb
 selfhost/tests/*.js
+selfhost/failtests/*.wyb
+selfhost/failtests/*.js
 selfhost/output.js
diff --git a/selfhost/binding.wyv b/selfhost/binding.wyv
index 295b46cb5..6013e2722 100644
--- a/selfhost/binding.wyv
+++ b/selfhost/binding.wyv
@@ -1,114 +1,157 @@
 import raw
-import bound
 import error
 import lexUtil
 import types
+import typesUtil
 import typecheck
-import subtyping
 import wyvern.collections.llist
 
 type List = llist.LinkedList
 type DeclType = types.DeclType
 
-def stringToType(s:String, ctx:bound.Context):types.Type
-    if (s == "Unit")
-            types.theUnit
-        else
-            val pred = ((b:DeclType) =>
-                val z = match b:
-                    tt:types.TypeType =>
-                        if (tt.name.name == s) { option.Some[types.TypeType](tt) } else { option.None[types.TypeType]() }
-                    default => option.None[types.TypeType]()
-                z
-            )
-            types.makeNominalType(types.findInDeclList[types.TypeType](ctx.bindings, pred).name)
-
-def bindDeclTypes(e:raw.Exp, context:bound.Context):DeclType = match e:
+def rawToType(s:raw.Type, ctx:types.Context):types.Type
+    val base = match s.base:
+        b:raw.Base => 
+            if (b.str == "Unit")
+                types.UnitType()
+              else 
+                if (b.str == "Bottom")
+                    types.BotType()
+                  else
+                    val pred = typesUtil.findTypePredicateFromStr(b.str)
+                    val L = typesUtil.findInDeclList[types.TypeType](ctx.bindings, pred).name
+                    types.NominalType(L)
+        path:raw.Path =>
+            val p = bindExpr(path.p,ctx)
+            types.PathType(p,path.t)
+    val refines = s.refines.map[types.DeclType](e => bindDeclTypes(e,ctx))
+    types.Type(base,refines)
+
+def bindDeclTypes(e:raw.Exp, context:types.Context):DeclType = match e:
     v:raw.ValType =>
         val b = types.Binding(v.name, context.counter)
-        types.ValType(b,stringToType(v.typ, context))
+        types.ValType(b,rawToType(v.typ, context))
     d:raw.DefDecl =>
         val b = types.Binding(d.name, context.counter)
-        val argtypes = d.args.map[types.Type]((e:raw.Arg) => stringToType(e.argTyp,context))
-        types.DefType(b, argtypes, stringToType(d.retTyp,context))
+
+        var newCtx:types.Context = context
+        def mapParams(args:List[raw.Arg]):List[types.ValType] = match args:
+            c:llist.Cons =>
+                val arg = types.ValType(types.Binding(c.value.arg,newCtx.counter),rawToType(c.value.argTyp,newCtx))
+                newCtx = newCtx.extend(arg)
+                llist.Cons[types.ValType](arg,mapParams(c.next))
+            n:llist.Nil => llist.Nil[types.ValType]()
+        val arglist = mapParams(d.args)
+        types.DefType(b, arglist, rawToType(d.retTyp,newCtx))
+    
     t:raw.TypeDecl =>
         val b = types.Binding(t.name, context.counter)
-        val nominalDecl = types.TypeType(b, types.makeNominalType(b))
+        val z = types.Binding(t.self, context.counter)
+        val nominalDecl = types.TypeType(b, z, llist.Nil[DeclType]())
+        val zVar = types.ValType(z,types.makeNominalType(b))
 
         val declSeq = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(t.decls)))
-        val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl)))
-        types.TypeType(b,types.makeRefines((declList)))
-
+        val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl).extend(zVar)))
+        types.TypeType(b,z,declList)
+    t:raw.TypeMem =>
+        val b = types.Binding(t.name, context.counter)
+        val bound:types.Bound = match t.bound:
+            a:raw.LEQ => types.LEQ()
+            a:raw.EQ  => types.EQ()
+            a:raw.GEQ => types.GEQ()
+        val typ = rawToType(t.tau, context)
+        types.MemberType(b, bound, typ)
+    s:raw.SubtypeDecl =>
+        types.SubtypeType(rawToType(s.subtype,context),rawToType(s.supertype,context))
     default       => error.report("unexpected construct", error.unknownLocation)
 
 def makeSeq(e:raw.Exp):raw.Seq = match e: //ensures that the whole expression is a Seq, in program order--actually all the raw Seqs are reversed
     s:raw.Seq => raw.Seq(s.exps.reverse())
     default => raw.Seq(llist.Singleton[raw.Exp](e))
 
-def bind(e:raw.Exp, parse: String -> raw.Exp):bound.Statement
-    bindStatement(makeSeq(e), bound.emptyContext(parse))
+def bind(e:raw.Exp, parse: String -> raw.Exp):types.Statement
+    bindTopLevel(e, types.emptyContext(parse))
 
-def bindStatement(e:raw.Seq, context:bound.Context):bound.Statement = match e.exps:
+def bindTopLevel(e:raw.Exp, context:types.Context):types.Statement
+    //add Unit type decl
+    val nameb = types.Binding("Unit",context.counter)
+    val zb = types.Binding("z",context.counter)
+    val unitTypeDecl = types.TypeDecl(nameb,zb,llist.Nil[DeclType]())
+    val unitDeclType = types.TypeType(nameb,zb,llist.Nil[DeclType]())
+
+    val program = bindStatement(makeSeq(e),context.extend(unitDeclType))
+    types.DeclStatement(unitTypeDecl,program)
+
+def bindStatement(e:raw.Seq, context:types.Context):types.Statement = match e.exps:
     c:llist.Cons => match c.next:
         cc:llist.Cons => 
-            val b:bound.Decl = bindDecl(c.value, context)
+            val b:types.Decl = bindDecl(c.value, context)
             val decl:DeclType = match b:
-                v:bound.Val =>
+                v:types.Val =>
                     types.ValType(v.binding, v.typ)
-                d:bound.Def =>
-                    types.DefType(d.binding, d.args.map[types.Type](e => e.argTyp), d.retTyp)
-                t:bound.TypeDecl =>
-                    types.TypeType(t.name, t.typ)
-                s:bound.SubtypeDecl =>
+                d:types.Def =>
+                    types.DefType(d.binding, d.args, d.retTyp)
+                t:types.TypeDecl =>
+                    types.TypeType(t.name, t.z, t.typ)
+                t:types.TypeEq =>
+                    types.MemberType(t.name, types.EQ(), t.typ)
+                s:types.SubtypeDecl =>
                     types.SubtypeType(s.subtype, s.supertype)
             val newCtx = context.extend(decl)
-            bound.DeclStatement(b, bindStatement(raw.Seq(c.next), newCtx))
-        default => bound.ExprStatement(bindExpr(c.value, context))
+            types.DeclStatement(b, bindStatement(raw.Seq(c.next), newCtx))
+        default => types.ExprStatement(bindExpr(c.value, context))
     default => error.report("empty statement",error.unknownLocation)
 
-def bindDecl(e:raw.Exp, context:bound.Context):bound.Decl = match e:
+def bindDecl(e:raw.Exp, context:types.Context):types.Decl = match e:
     v:raw.Val => 
         val b = types.Binding(v.name, context.counter)
         val body = bindExpr(v.exp, context)
         val expType = typecheck.typecheckExpr(body, context.bindings)
-        bound.Val(b, expType, body)
+        types.Val(b, expType, body)
     v:raw.ValAnnot =>
         val b = types.Binding(v.name, context.counter)
         val body = bindExpr(v.exp, context)
         val expType = typecheck.typecheckExpr(body, context.bindings)
-        val annotType = stringToType(v.typ,context)
-        if (!subtyping.isSubtype(expType,annotType,context.bindings))
+        val annotType = rawToType(v.typ,context)
+        if (!typecheck.isSubtype(expType,annotType,context.bindings))
             error.report("val expr doesn't match annotation",error.unknownLocation)
-        bound.Val(b, annotType, body)
+        types.Val(b, annotType, body)
     d:raw.Def =>
         val b = types.Binding(d.name, context.counter)
-        def rawToBoundArg(a:raw.Arg):bound.Arg
-            val argb = types.Binding(a.arg, context.counter)
-            bound.Arg(argb,stringToType(a.argTyp,context))
-        val arglist = d.args.map[bound.Arg](a => rawToBoundArg(a))
-        val argtypes = arglist.map[types.Type]((a:bound.Arg) => a.argTyp)
-        val argdecls = arglist.map[types.ValType]((a:bound.Arg) => types.ValType(a.arg,a.argTyp))
 
-        val methodDecl = types.DefType(b, argtypes, stringToType(d.retTyp,context))
+        var newCtx:types.Context = context
+        def mapParams(args:List[raw.Arg]):List[types.ValType] = match args:
+            c:llist.Cons =>
+                val arg = types.ValType(types.Binding(c.value.arg,newCtx.counter),rawToType(c.value.argTyp,newCtx))
+                newCtx = newCtx.extend(arg)
+                llist.Cons[types.ValType](arg,mapParams(c.next))
+            n:llist.Nil => llist.Nil[types.ValType]()
+        val arglist = mapParams(d.args)
+
+        val methodDecl = types.DefType(b, arglist, rawToType(d.retTyp,newCtx))
+        newCtx.extend(methodDecl)
 
         val defn = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(d.body)))
-        bound.Def(b, arglist, methodDecl.retTyp, bindStatement(defn, context.extend(methodDecl).extendList(argdecls)))
+        types.Def(b, arglist, methodDecl.retTyp, bindStatement(defn, newCtx))
     t:raw.TypeDecl =>
         val b = types.Binding(t.name, context.counter)
-        val nominalDecl = types.TypeType(b, types.makeNominalType(b))
+        val z = types.Binding(t.self, context.counter)
+        val nominalDecl = types.TypeType(b, z, llist.Nil[DeclType]())
+        val zVar = types.ValType(z,types.makeNominalType(b))
 
         val declSeq = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(t.decls)))
-        val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl)))
-        bound.TypeDecl(b, types.makeRefines(declList))
-    t:raw.TypeAlias =>
+        val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl).extend(zVar)))
+
+        types.TypeDecl(b, z, declList)
+    t:raw.TypeMem =>
         val b = types.Binding(t.name, context.counter)
-        val aliasType = stringToType(t.alias, context)
-        bound.TypeDecl(b, aliasType)
+        val typ = rawToType(t.tau, context)
+        types.TypeEq(b, typ)
     s:raw.SubtypeDecl =>
-        bound.SubtypeDecl(stringToType(s.subtype,context),stringToType(s.supertype,context))
+        types.SubtypeDecl(rawToType(s.subtype,context),rawToType(s.supertype,context))
     default => error.report("not a declaration: " + raw.expToString(e),error.unknownLocation)
 
-def bindExpr(e:raw.Exp, context:bound.Context):bound.Exp = match e:
+def bindExpr(e:raw.Exp, context:types.Context):types.Exp = match e:
     v:raw.Var    => 
         val pred = ((b:DeclType) =>
             val z = match b:
@@ -117,14 +160,14 @@ def bindExpr(e:raw.Exp, context:bound.Context):bound.Exp = match e:
                 default => option.None[types.ValType]()
             z
         )
-        val binding = types.findInDeclList[types.ValType](context.bindings, pred).name
-        bound.Var(binding)
+        val binding = typesUtil.findInDeclList[types.ValType](context.bindings, pred).name
+        types.Var(binding)
     a:raw.App    => 
         val rec = bindExpr(a.func, context)
         val arg = bindExpr(a.arg, context)
-        val app = bound.Call(rec, "apply", llist.Singleton[bound.Exp](arg))
+        val app = types.Call(rec, "apply", llist.Singleton[types.Exp](arg))
         match rec:
-            f:bound.Field => 
+            f:types.Field => 
                 //check if field is actually a method
                 val recType = typecheck.typecheckExpr(f.receiver,context.bindings)
                 val pred = ((b:types.DeclType) =>
@@ -133,38 +176,38 @@ def bindExpr(e:raw.Exp, context:bound.Context):bound.Exp = match e:
                         default => false
                     z
                 )
-                val searchMethod = llist.find[types.DeclType](types.unfoldType(recType,context.bindings), pred)
+                val searchMethod = llist.find[types.DeclType](typecheck.unfoldType(recType,context.bindings).decls, pred)
                 match searchMethod:
-                    s:option.Some => bound.Call(f.receiver, f.field, llist.Singleton[bound.Exp](arg))
+                    s:option.Some => types.Call(f.receiver, f.field, llist.Singleton[types.Exp](arg))
                     default => app
             default => app
     l:raw.Lambda =>
         val argb = types.Binding(l.name, context.counter)
-        val argDecl = types.ValType(argb, stringToType(l.argTyp, context))
+        val argDecl = types.ValType(argb, rawToType(l.argTyp, context))
 
         val newCtx = context.extend(argDecl)
         val boundExp = bindExpr(l.body, newCtx)
         val expType = typecheck.typecheckExpr(boundExp, newCtx.bindings)
 
         val applyb = types.Binding("apply", context.counter)
-        val decl = types.DefType(applyb, llist.Singleton[types.Type](argDecl.typ), expType)
-        val defDeclaration:bound.Decl = bound.Def(applyb, llist.Singleton[bound.Arg](bound.Arg(argb,argDecl.typ)), expType, bound.ExprStatement(boundExp))
+        val decl = types.DefType(applyb, llist.Singleton[types.ValType](types.ValType(argb,argDecl.typ)), expType)
+        val defDeclaration:types.Decl = types.Def(applyb, llist.Singleton[types.ValType](types.ValType(argb,argDecl.typ)), expType, types.ExprStatement(boundExp))
 
         val thisb = types.Binding("_this", context.counter)
         val thisType = types.makeRefines(llist.Singleton[DeclType](decl))
-        bound.New(thisb, thisType, llist.Singleton[bound.Decl](defDeclaration))
+        types.New(thisb, thisType, llist.Singleton[types.Decl](defDeclaration))
     c:raw.Call   => 
-        bound.Call(bindExpr(c.receiver, context), c.name, c.args.map[bound.Exp](e => bindExpr(e, context)))
+        types.Call(bindExpr(c.receiver, context), c.name, c.args.map[types.Exp](e => bindExpr(e, context)))
     f:raw.Field  =>
-        bound.Field(bindExpr(f.receiver, context), f.field)
+        types.Field(bindExpr(f.receiver, context), f.field)
     n:raw.New    =>
         val b:types.Binding = types.Binding(n.thisName, context.counter)
-        val typ:types.Type = stringToType(n.typeName, context)
+        val typ:types.Type = rawToType(n.typeName, context)
         val thisDecl = types.ValType(b, typ)
 
         val parsedBody = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(n.body)))
-        val boundDecls:List[bound.Decl] = parsedBody.exps.map[bound.Decl]((e:raw.Exp) => bindDecl(e, context.extend(thisDecl)))
-        bound.New(b, typ, boundDecls)
-    i:raw.Integer     => bound.Integer(i.str)
-    u:raw.UnitVal     => bound.UnitVal()
+        val boundDecls:List[types.Decl] = parsedBody.exps.map[types.Decl]((e:raw.Exp) => bindDecl(e, context.extend(thisDecl)))
+        types.New(b, typ, boundDecls)
+    i:raw.Integer     => types.Integer(i.str)
+    u:raw.UnitVal     => types.UnitVal()
     default      => error.report("unexpected construct in bindexpr: " + raw.expToString(e), error.unknownLocation)
diff --git a/selfhost/bound.wyv b/selfhost/bound.wyv
index 093d6ee7e..8618c4ce4 100644
--- a/selfhost/bound.wyv
+++ b/selfhost/bound.wyv
@@ -1,6 +1,5 @@
 module bound
 
-import raw
 import types
 import wyvern.collections.llist
 type List = llist.LinkedList
@@ -8,64 +7,22 @@ type Counter = types.Counter
 type Binding = types.Binding
 type DeclType = types.DeclType
 
-resource type Context
-    val bindings:List[DeclType]
-    val counter:Counter
-    val parse:String -> raw.Exp
-    def extend(b:DeclType):Context
-    def extendList(b:List[DeclType]):Context
 
-def Context(bs:List[DeclType], c:Counter, p:String -> raw.Exp) : Context = new
-    val bindings = bs
-    val counter = c
-    val parse = p
-    def extend(b:DeclType):Context
-        Context(llist.Cons[DeclType](b, bs), c, p)
-    def extendList(b:List[DeclType]):Context
-        val newBindings = b.append(bs)
-        Context(newBindings,c,p)
-    
-def emptyContext(p:String -> raw.Exp):Context = Context(llist.Nil[DeclType](), types.Counter(), p)
-
-type Arg
-    val arg:Binding
-    val argTyp:types.Type
-def Arg(arg:Binding,argTyp:types.Type):Arg = new
-    val arg = arg
-    val argTyp = argTyp
-
-datatype Statement
-    DeclStatement(decl:Decl, stmt:Statement)
-    ExprStatement(exp:Exp)
-
-datatype Decl
-    Val(binding:Binding, typ:types.Type, exp:Exp)
-    Def(binding:Binding, args:List[Arg], retTyp:types.Type, body:Statement)
-    TypeDecl(name:Binding, typ:types.Type)
-    SubtypeDecl(subtype:types.Type, supertype:types.Type)
-
-datatype Exp
-    Var(binding:Binding)
-    Call(receiver:Exp, name:String, args:List[Exp])
-    Field(receiver:Exp, field:String)
-    New(binding:Binding, typ:types.Type, body:List[Decl])
-    Integer(str:String)
-    UnitVal()
-
-def lowerStatement(stmt:Statement):Statement = match stmt:
-    d:DeclStatement => DeclStatement(lowerDecl(d.decl), lowerStatement(d.stmt))
-    e:ExprStatement => ExprStatement(lowerExp(e.exp))
-
-def lowerDecl(decl:Decl):Decl = match decl:
-    v:Val         => Val(v.binding, v.typ, lowerExp(v.exp))
-    d:Def         => Def(d.binding, d.args, d.retTyp, lowerStatement(d.body))
-    t:TypeDecl    => t
-    s:SubtypeDecl => s
-
-def lowerExp(exp:Exp):Exp = match exp:
-    v:Var     => v
-    c:Call    => Call(lowerExp(c.receiver), c.name, c.args.map[Exp](e => lowerExp(e)))
-    f:Field   => Field(lowerExp(f.receiver), f.field)
-    n:New     => New(n.binding, n.typ, n.body.map[Decl](d => lowerDecl(d)))
-    i:Integer => i
-    u:UnitVal => u
+def lowerStatement(stmt:types.Statement):types.Statement = match stmt:
+    d:types.DeclStatement => types.DeclStatement(lowerDecl(d.decl), lowerStatement(d.stmt))
+    e:types.ExprStatement => types.ExprStatement(lowerExp(e.exp))
+
+def lowerDecl(decl:types.Decl):types.Decl = match decl:
+    v:types.Val         => types.Val(v.binding, v.typ, lowerExp(v.exp))
+    d:types.Def         => types.Def(d.binding, d.args, d.retTyp, lowerStatement(d.body))
+    t:types.TypeDecl    => t
+    s:types.SubtypeDecl => s
+    m:types.TypeEq  => m
+
+def lowerExp(exp:types.Exp):types.Exp = match exp:
+    v:types.Var     => v
+    c:types.Call    => types.Call(lowerExp(c.receiver), c.name, c.args.map[types.Exp](e => lowerExp(e)))
+    f:types.Field   => types.Field(lowerExp(f.receiver), f.field)
+    n:types.New     => types.New(n.binding, n.typ, n.body.map[types.Decl](d => lowerDecl(d)))
+    i:types.Integer => i
+    u:types.UnitVal => u
diff --git a/selfhost/failtests/AB.wyv b/selfhost/failtests/AB.wyv
new file mode 100644
index 000000000..5f86bc154
--- /dev/null
+++ b/selfhost/failtests/AB.wyv
@@ -0,0 +1,17 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type A:z:
+    type T >= Bottom
+   
+type B:z:
+    type S <= Unit
+    type T = A {type T >= B {type S = B {type S = z.S}}}
+subtype B extends A
+
+val bad:A {type T >= B {type S = Int}} = new this:B {type S = Int}:
+    type S = Int
+    type T = A {type T >= B {type S = B {type S = this.S}}}
+
+0  
diff --git a/selfhost/failtests/badsubtype.wyv b/selfhost/failtests/badsubtype.wyv
new file mode 100644
index 000000000..59b21d7ff
--- /dev/null
+++ b/selfhost/failtests/badsubtype.wyv
@@ -0,0 +1,15 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type A:z:
+    type T >= Int
+    val a:z.T
+
+type B:z:
+    type T <= Int
+    val a:z.T
+
+subtype B extends A
+
+0
diff --git a/selfhost/failtests/badsubtype2.wyv b/selfhost/failtests/badsubtype2.wyv
new file mode 100644
index 000000000..ae87248bb
--- /dev/null
+++ b/selfhost/failtests/badsubtype2.wyv
@@ -0,0 +1,19 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type A:z:
+    type T >= Int
+    val a:z.T
+
+type B:z:
+    type T <= Int
+    val a:z.T
+
+type C:z:
+    val a:Int    
+
+subtype Unit {val a:Int} extends C
+subtype Unit {type T <= Int, val a:Int} extends B
+
+0
diff --git a/selfhost/failtests/eq.wyv b/selfhost/failtests/eq.wyv
new file mode 100644
index 000000000..7edec5c2f
--- /dev/null
+++ b/selfhost/failtests/eq.wyv
@@ -0,0 +1,22 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Eq:z:
+    type E <= Unit
+
+type List:z:
+    type T <= Unit 
+    type E = List {type T <= Eq {type E >= z.T}}
+subtype List extends Eq
+
+type Tree:z:
+    type T = Tree
+    type E = List {type T <= Eq {type E >= z.T}}
+subtype Tree extends List
+
+val bad:Eq {type E >= Tree} = new this:Tree:
+    type T = Tree
+    type E = List {type T <= Eq {type E >= this.T}}
+
+0  
diff --git a/selfhost/main.wyv b/selfhost/main.wyv
index 1025d1fb0..542b23d51 100644
--- a/selfhost/main.wyv
+++ b/selfhost/main.wyv
@@ -17,8 +17,12 @@ import bound
 import toBytecode
 import wyvern.collections.llist
 import types
+import typesUtil
 import typecheck
 
+import wyvern.exception
+import error
+
 // instantiate imports and create aliases
 type List = llist.LinkedList
 val wyvernLexer = wyvernLexer(js, regexUtils)
@@ -58,23 +62,29 @@ def parse(s:String):raw.Exp
     pars.results.get(0)
 
 stdout.print("Binding...\n")
-val boundExp:bound.Statement = binding.bind(parser.results.get(0), s => parse(s))
-/*
-val boundExp : exception.Answer[bound.Statement,exception.Exception] = exception.try[bound.Statement](() => binding.bind(parser.results.get(0), s => parse(s)))
-match boundExp:
-    s1: exception.Success =>
-        stdout.print("success\n")
-    f1: exception.Failure =>
-        match f1.exception:
-            exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
-            default => stdout.print("unexpected exception thrown\n")
-*/
+val boundExp:types.Statement = binding.bind(parser.results.get(0), s => parse(s))
+//val boundExp : exception.Answer[types.Statement,exception.Exception] = exception.try[types.Statement](() => binding.bind(parser.results.get(0), s => parse(s)))
+//match boundExp:
+//    s1: exception.Success =>
+//        stdout.print("binding success\n")
+//        val tc:exception.Answer[types.Type,exception.Exception] = exception.try[types.Type](() => typecheck.typecheck(s1.value))
+//        match tc:
+//            s1: exception.Success =>
+//                stdout.print("type: " + typesUtil.typeToString(s1.value) + "\n")
+//            f1: exception.Failure =>
+//                match f1.exception:
+//                    exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
+//                    default => stdout.print("unexpected exception thrown\n")
+//    f1: exception.Failure =>
+//        match f1.exception:
+//            exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
+//            default => stdout.print("unexpected exception thrown\n")
 
 val tc = typecheck.typecheck(boundExp)
-stdout.print("type: " + types.typeToString(tc) + "\n")
+stdout.print("type: " + typesUtil.typeToString(tc) + "\n")
 
 stdout.print("Lowering...\n")
-val ooExp:bound.Statement = bound.lowerStatement(boundExp)
+val ooExp:types.Statement = bound.lowerStatement(boundExp)
 
 val outputFileName = string.replace(fileName, ".wyv", ".wyb")
 
diff --git a/selfhost/raw.wyv b/selfhost/raw.wyv
index cfb9fd3a5..67a731940 100644
--- a/selfhost/raw.wyv
+++ b/selfhost/raw.wyv
@@ -5,56 +5,82 @@ type List = llist.LinkedList
 
 type Arg
     val arg:String
-    val argTyp:String
-def Arg(arg:String,argTyp:String):Arg = new
+    val argTyp:Type
+def Arg(arg:String,argTyp:Type):Arg = new
     val arg = arg
     val argTyp = argTyp
 
+datatype Bound
+    EQ()
+    LEQ()
+    GEQ()
+
+datatype BaseType
+    Base(str:String)
+    Path(p:Exp,t:String)
+type Type
+    val base:BaseType
+    val refines:List[Exp]
+def Type(b:BaseType, r:List[Exp]):Type = new
+    val base = b
+    val refines = r
+
 datatype Exp
     Var(name:String)
     App(func:Exp, arg:Exp)
-    Lambda(name:String, argTyp:String, body:Exp)
+    Lambda(name:String, argTyp:Type, body:Exp)
     Call(receiver:Exp, name:String, args:List[Exp])
     Field(receiver:Exp, field:String)
     Val(name:String, exp:Exp)
-    ValAnnot(name:String, typ:String, exp:Exp)
-    Def(name:String, args:List[Arg], retTyp:String, body:String)
-    ValType(name:String, typ:String)
-    TypeDecl(name:String, decls:String)
-    TypeAlias(name:String, alias:String)
-    DefDecl(name:String, args:List[Arg], retTyp:String)
-    SubtypeDecl(subtype:String, supertype:String)
-    New(thisName:String, typeName:String, body:String)
+    ValAnnot(name:String, typ:Type, exp:Exp)
+    Def(name:String, args:List[Arg], retTyp:Type, body:String)
+    ValType(name:String, typ:Type)
+    TypeDecl(name:String, self:String, decls:String)
+    TypeMem(name:String, bound:Bound, tau:Type)
+    DefDecl(name:String, args:List[Arg], retTyp:Type)
+    SubtypeDecl(subtype:Type, supertype:Type)
+    New(thisName:String, typeName:Type, body:String)
     Seq(exps:List[Exp])
     Integer(str:String)    
     UnitVal()
 
 def argsToString(args:List[Arg]):String = match args:
     c:llist.Cons => match c.next:
-        n:llist.Nil => c.value.arg + ":" + c.value.argTyp
-        default => c.value.arg + ":" + c.value.argTyp + ", " + argsToString(c.next)
+        n:llist.Nil => c.value.arg + ":" + typeToString(c.value.argTyp)
+        default => c.value.arg + ":" + typeToString(c.value.argTyp) + ", " + argsToString(c.next)
 
 def callListToString(args:List[Exp]):String = match args:
     c:llist.Cons => match c.next:
         n:llist.Nil => expToString(c.value)
         default => expToString(c.value) + ", " + callListToString(c.next)
-    default => "call list empty!"
+    default => ""
+
+def typeToString(t:Type):String
+    val baseString = match t.base:
+        b:Base => b.str    
+        p:Path => expToString(p.p) + "." + p.t
+    baseString + " {" + callListToString(t.refines) + "}"
+
+def boundToString(b:Bound):String = match b:
+    e:EQ  => "="
+    e:LEQ => "<="
+    e:GEQ => ">="
 
 def expToString(e:Exp):String = match e:
     v:Var    => v.name
     a:App    => "((" + expToString(a.func) + ") (" + expToString(a.arg) + "))"
-    l:Lambda => l.name + ":" + l.argTyp + " => " + expToString(l.body)
+    l:Lambda => l.name + ":" + typeToString(l.argTyp) + " => " + expToString(l.body)
     c:Call   => expToString(c.receiver) + "." + c.name + "(" + callListToString(c.args) + ")" 
     f:Field  => expToString(f.receiver) + "." + f.field
     v:Val    => "val " + v.name + " = " + expToString(v.exp)
-    v:ValAnnot    => "val " + v.name + ":" + v.typ + " = " + expToString(v.exp)
-    d:Def    => "def " + d.name + "(" + argsToString(d.args) + "):" + d.retTyp + ":\n" + d.body
-    v:ValType => "val " + v.name + ": " + v.typ
-    t:TypeDecl => "type " + t.name + ":\n" + t.decls
-    t:TypeAlias => "type " + t.name + " = " + t.alias
-    d:DefDecl => "def " + d.name + "(" + argsToString(d.args) + ")" + d.retTyp
-    s:SubtypeDecl => "subtype " + s.subtype + " extends " + s.supertype
-    n:New => "new " + n.thisName + ":" + n.typeName + ":\n" + n.body
+    v:ValAnnot    => "val " + v.name + ":" + typeToString(v.typ) + " = " + expToString(v.exp)
+    d:Def    => "def " + d.name + "(" + argsToString(d.args) + "):" + typeToString(d.retTyp) + ":\n" + d.body
+    v:ValType => "val " + v.name + ": " + typeToString(v.typ)
+    t:TypeDecl => "type " + t.name + ":" + t.self + ":\n" + t.decls
+    t:TypeMem => "type " + t.name + " " + boundToString(t.bound) + " " + typeToString(t.tau)
+    d:DefDecl => "def " + d.name + "(" + argsToString(d.args) + ")" + typeToString(d.retTyp)
+    s:SubtypeDecl => "subtype " + typeToString(s.subtype) + " extends " + typeToString(s.supertype)
+    n:New => "new " + n.thisName + ":" + typeToString(n.typeName) + ":\n" + n.body
     s:Seq    => s.exps.foldRight[String]((e:Exp, s:String) => s + "\n" + expToString(e), "")
     i:Integer => i.str
     u:UnitVal => "()"
diff --git a/selfhost/subtyping.wyv b/selfhost/subtyping.wyv
deleted file mode 100644
index 65fff2767..000000000
--- a/selfhost/subtyping.wyv
+++ /dev/null
@@ -1,122 +0,0 @@
-module subtyping
-
-import types
-import error
-import wyvern.collections.llist
-import wyvern.option
-type List = llist.LinkedList
-type Binding = types.Binding
-type Type = types.Type
-type DeclType = types.DeclType
-type BaseType = types.BaseType
-type ValType = types.ValType
-type TypeType = types.TypeType
-type DefType = types.DefType
-type SubtypeType = types.SubtypeType
-type UnitType = types.UnitType
-type NominalType = types.NominalType
-
-//Check if two lists of arguments line up in the right way
-def checkArgList(xs:List[Type],ys:List[Type],pred:Type->Type->Boolean):Boolean
-    if (xs.size() == ys.size())
-        def f(xs:List[Type],ys:List[Type]):Boolean = match xs:
-            a:llist.Cons => match ys:
-                b:llist.Cons =>   
-                    (pred(a.value)(b.value)) && f(a.next,b.next)
-            default => true
-        f(xs,ys)
-      else
-        false
-
-//Check if for each y in ys there is an x in xs s.t. (pred x y) is true
-def checkDeclList(xs:List[DeclType],ys:List[DeclType],pred:DeclType->DeclType->Boolean):Boolean
-    def isValid(d:DeclType):Boolean
-        val search = llist.find[DeclType](xs, (e:DeclType) => pred(e)(d))
-        match search:
-            s:option.Some => true
-            default => false
-    ys.foldRight[Boolean]((x:DeclType,y:Boolean) => isValid(x) && y, true)
-
-def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean
-    match a:
-        v:ValType => match b:
-            u:ValType => v.name.name == u.name.name && equalType(v.typ,u.typ,gamma)
-            default => false
-        t:TypeType => match b:
-            u:TypeType => 
-                val tt = types.unfoldType(types.makeNominalType(t.name),gamma)
-                val uu = types.unfoldType(types.makeNominalType(u.name),gamma)
-                t.name.name == u.name.name && checkDeclList(tt,uu,x=>y=>equalDeclType(x,y,gamma))
-            default => false
-        d:DefType => match b:
-            u:DefType => 
-                val pred = x:Type => y:Type => equalType(x,y,gamma)
-                d.name.name == u.name.name && checkArgList(d.args,u.args,pred) && equalType(d.retTyp,u.retTyp,gamma)
-            default => false
-
-def equalBaseType(a:BaseType, b:BaseType, gamma:List[DeclType]):Boolean = match a:
-    u:UnitType => match b:
-        v:UnitType => true
-        default => false
-    n:NominalType => match b:
-        v:NominalType => 
-            def getNominalRoot(bind:Binding):Binding
-                val pred = types.findTypePredicate(bind)
-                val par = types.findInDeclList[TypeType](gamma, pred)
-                match par.unfld.base:
-                    u:UnitType    => bind
-                    n:NominalType => getNominalRoot(n.L)
-            types.equalBinding(getNominalRoot(n.L),getNominalRoot(v.L))
-        default => false
-
-def equalType(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
-    val pred = x:DeclType => y:DeclType => equalDeclType(x,y,gamma)
-    equalBaseType(t1.base,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,pred)
-
-def isSubtypeDeclList(xs:List[DeclType], ys:List[DeclType], gamma:List[DeclType]):Boolean
-    checkDeclList(xs,ys,x=>y=>isSubtypeDecl(x,y,gamma))
-
-def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
-    v:ValType => match b:    
-        u:ValType => v.name.name == u.name.name && isSubtype(v.typ,u.typ,gamma)
-        default => false
-    t:TypeType => match b:
-        u:TypeType => equalDeclType(a,b,gamma)
-        default => false
-    d:DefType => match b:
-        u:DefType => 
-            val pred = x:Type => y:Type => isSubtype(x,y,gamma)
-            d.name.name == u.name.name && checkArgList(u.args,d.args,pred) && isSubtype(d.retTyp,u.retTyp,gamma)
-        default => false
-
-def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
-    if (equalType(t2,types.theUnit,gamma))
-        true
-      else
-        isSubtypeBase(t1,t2.base,gamma) && isSubtypeDeclList(t1.refines,t2.refines,gamma)
-
-def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
-    val b1 = types.Type(t1.base,llist.Nil[DeclType]())
-    val b2 = types.Type(t2,llist.Nil[DeclType]())
-    if (equalType(b1,b2,gamma))
-        true
-      else
-        val pred = ((b:DeclType) =>
-            val z = match b:
-                s:types.SubtypeType =>
-                    equalType(types.makeBase(s.subtype.base),types.makeBase(t1.base),gamma) \
-                 && isSubtypeDeclList(t1.refines,s.subtype.refines,gamma) \
-                 && isSubtypeBase(types.Type(s.supertype.base,t1.refines),t2,gamma)
-                default => false
-            z
-        )
-        val search = llist.find[DeclType](gamma,pred)
-        match search:
-            s:option.Some => true
-            default => false
-
-def checkSubtypeWF(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
-    val ua = types.unfoldType(t1,gamma)
-    val ub = types.unfoldType(t2,gamma)
-    val newgamma = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma)
-    isSubtypeDeclList(ua,ub,newgamma)
diff --git a/selfhost/tests/aliasTest.wyv b/selfhost/tests/aliasTest.wyv
deleted file mode 100644
index ce8eb787d..000000000
--- a/selfhost/tests/aliasTest.wyv
+++ /dev/null
@@ -1,13 +0,0 @@
-type Int:
-    def +(i:Int):Int
-    def -(i:Int):Int
- 
-type A = Int
-type B = Int
-type C = B
-type D = C
-type E = A
-
-val calc = x:D => y:E => x + y
-val id = x:C => x
-calc (id 3) (id 2)
diff --git a/selfhost/tests/arity.wyv b/selfhost/tests/arity.wyv
index cd52d392a..643e8b138 100644
--- a/selfhost/tests/arity.wyv
+++ b/selfhost/tests/arity.wyv
@@ -1,8 +1,8 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type A:
+type A:z:
     def f(x:Int):Int
     def g(x:Int,y:Int,z:Int):Int
 
diff --git a/selfhost/tests/cloneable.wyv b/selfhost/tests/cloneable.wyv
new file mode 100644
index 000000000..b28a3a8ca
--- /dev/null
+++ b/selfhost/tests/cloneable.wyv
@@ -0,0 +1,26 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Cloneable:z:
+    type T <= Unit
+    def clone(u:Unit):z.T
+
+type String:z:
+    type T <= String
+    def clone(u:Unit):z.T
+subtype String extends Cloneable
+
+type A:z:
+    def makeClone(arg:Cloneable):arg.T
+val a = new this:A:
+    def makeClone(arg:Cloneable):arg.T:
+        arg.clone(())
+
+val s = new this:String:
+    type T <= String
+    def clone(u:Unit):this.T:
+        a.makeClone(this)
+
+
+a.makeClone(s)
diff --git a/selfhost/tests/counter.wyv b/selfhost/tests/counter.wyv
index a1710c7e8..d8c9c020d 100644
--- a/selfhost/tests/counter.wyv
+++ b/selfhost/tests/counter.wyv
@@ -1,12 +1,12 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Counter:
+type Counter:z:
     val a:Int
     def next(u:Unit):Counter
 
-type X:
+type X:z:
     def makeCounter(b:Int):Counter
 
 val x = new self:X:
diff --git a/selfhost/tests/fib.wyv b/selfhost/tests/fib.wyv
index 6940cc0e0..4ac5dd056 100644
--- a/selfhost/tests/fib.wyv
+++ b/selfhost/tests/fib.wyv
@@ -1,13 +1,13 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Fib:
+type Fib:z:
     val a1:Int
     val a2:Int
     def next(u:Unit):Fib
 
-type X:
+type X:z:
     def makeFib(x:Int,y:Int):Fib
 
 val x = new self:X:
diff --git a/selfhost/tests/ipair.wyv b/selfhost/tests/ipair.wyv
new file mode 100644
index 000000000..9c8dd5014
--- /dev/null
+++ b/selfhost/tests/ipair.wyv
@@ -0,0 +1,18 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Pair:z:
+	type S <= Unit
+	type T <= Unit
+
+type IPair:z:
+	type S = Int
+	type T <= Unit
+subtype IPair extends Pair
+
+val ok:Pair{type S = Int, type T = Int} = new this:IPair {type T = Int}:
+	type S = Int
+	type T = Int
+
+ok
diff --git a/selfhost/tests/lambdaTest.wyv b/selfhost/tests/lambdaTest.wyv
index 4fc9ec6c7..def17f2f3 100644
--- a/selfhost/tests/lambdaTest.wyv
+++ b/selfhost/tests/lambdaTest.wyv
@@ -1,7 +1,7 @@
-type Int:
+type Int:z:
      def +(i:Int):Int
      def -(i:Int):Int
 
 val succ = x:Int => x + 1
 val fst = x:Int => y:Int => x
-fst 7
+fst
diff --git a/selfhost/tests/list.wyv b/selfhost/tests/list.wyv
new file mode 100644
index 000000000..a842b7f53
--- /dev/null
+++ b/selfhost/tests/list.wyv
@@ -0,0 +1,60 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Monoid:z:
+    type T <= Unit
+    val id:z.T
+    def op(a:z.T, b:z.T):z.T
+
+val Sum = new this:Monoid {type T = Int}:
+    type T = Int
+    val id:this.T = 0
+    def op(a:this.T, b:this.T):this.T:
+        a + b
+
+type List:z:
+    type T <= Unit
+    def reduce(m:Monoid {type T >= z.T}):m.T
+
+type Nil:z:
+    type T <= Unit
+    def reduce(m:Monoid {type T >= z.T}):m.T
+subtype Nil extends List
+
+type Cons:z:
+    type T <= Unit
+    val value:z.T
+    val next:List {type T = z.T}
+    def reduce(m:Monoid {type T >= z.T}):m.T
+subtype Cons extends List
+
+type Param:z:
+    type A <= Unit
+
+type AA:z:
+    def makeNil(a:Param):List {type T = a.A}
+    def makeCons(a:Param, x:a.A, xs:List {type T = a.A}):List {type T = a.A}
+
+val aa = new this:AA:
+    def makeNil(a:Param):List {type T = a.A}:
+        new this:Nil {type T = a.A}:
+            type T = a.A
+            def reduce(m:Monoid {type T >= this.T}):m.T:
+                m.id
+
+    def makeCons(a:Param, x:a.A, xs:List {type T = a.A}):List {type T = a.A}:
+        new this:Cons {type T = a.A}:
+            type T = a.A
+            val value = x
+            val next = xs
+            def reduce(m:Monoid {type T >= this.T}):m.T:
+                m.op(this.value,this.next.reduce(m))
+
+val IntP = new this:Param {type A = Int}:
+    type A = Int
+
+val IntNil = aa.makeNil(IntP)
+val l1 = aa.makeCons(IntP,3,IntNil)
+val l2 = aa.makeCons(IntP,4,l1)
+l2.reduce(Sum)
diff --git a/selfhost/tests/loop.wyv b/selfhost/tests/loop.wyv
index 2951a56a5..c0c69f4cb 100644
--- a/selfhost/tests/loop.wyv
+++ b/selfhost/tests/loop.wyv
@@ -1,8 +1,8 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type X:
+type X:z:
     def f(x:Int):Int
     val temp:Int
 
diff --git a/selfhost/tests/monoid.wyv b/selfhost/tests/monoid.wyv
new file mode 100644
index 000000000..aa4c78b23
--- /dev/null
+++ b/selfhost/tests/monoid.wyv
@@ -0,0 +1,29 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Semi:z:
+    type T <= Unit
+    def op(a:z.T, b:z.T):z.T
+
+type Monoid:z:
+    type T <= Unit
+    val id:z.T
+    def op(a:z.T, b:z.T):z.T
+subtype Monoid extends Semi
+
+val sum = new this:Monoid {type T = Int}:
+    type T = Int
+    val id:this.T = 0
+    def op(a:this.T, b:this.T):this.T:
+        a + b
+
+type Util:z:
+    def apply3(s:Semi, a:s.T, b:s.T, c:s.T):s.T
+
+val util = new this:Util:
+    def apply3(s:Semi, a:s.T, b:s.T, c:s.T):s.T:
+        s.op(a,s.op(b,c))
+
+val ans = util.apply3(sum,1,2,3)
+ans
diff --git a/selfhost/tests/newtest.wyv b/selfhost/tests/newtest.wyv
index 3a08c3c8f..4fc79635a 100644
--- a/selfhost/tests/newtest.wyv
+++ b/selfhost/tests/newtest.wyv
@@ -1,8 +1,8 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Foo:
+type Foo:z:
     def sum(x:Int):Int
     val a:Int
 
@@ -11,8 +11,7 @@ val foo = new this:Foo:
         this.a + x    
     val a = 5
 
-type Bar = Foo
-val bar = new this:Bar:
+val bar = new this:Foo:
     def sum(x:Int):Int:
         this.a + x    
     val a = 5
diff --git a/selfhost/tests/nomtype.wyv b/selfhost/tests/nomtype.wyv
new file mode 100644
index 000000000..82ec03ce2
--- /dev/null
+++ b/selfhost/tests/nomtype.wyv
@@ -0,0 +1,14 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type A:z:    
+    type X:y:
+        val a:Int
+
+type B:z:    
+    type X:z:
+        val a:Int
+subtype B extends A
+
+0
diff --git a/selfhost/tests/object.wyv b/selfhost/tests/object.wyv
index 0fb8c858e..9daf79c53 100644
--- a/selfhost/tests/object.wyv
+++ b/selfhost/tests/object.wyv
@@ -1,15 +1,15 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type List:
+type List:z:
     def sum(u:Unit):Int
 
-type Empty:
+type Empty:z:
     def sum(u:Unit):Int
 subtype Empty extends List
 
-type Node:
+type Node:z:
     def sum(u:Unit):Int
     val next:List
 subtype Node extends List
diff --git a/selfhost/tests/pair.wyv b/selfhost/tests/pair.wyv
new file mode 100644
index 000000000..8f502c72a
--- /dev/null
+++ b/selfhost/tests/pair.wyv
@@ -0,0 +1,35 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Pair:z:
+    type S <= Unit
+    type T <= Unit
+    val fst:z.S
+    val snd:z.T
+
+val p1 = new this:Pair {type S = Int, type T = Unit}:
+    type S = Int
+    type T = Unit
+    val fst:this.S = 3
+    val snd:this.T = ()
+
+type Param:z:
+    type A >= Int
+val IntP = new this:Param {type A = Int}:
+    type A = Int
+val UnitP = new this:Param {type A = Unit}:
+    type A = Unit
+
+type AA:z:
+    def swapPair(a:Param, b:Param, pair:Pair {type S = a.A, type T = b.A}):Pair {type S = b.A, type T = a.A}
+
+val aa = new this:AA:
+    def swapPair(a:Param, b:Param, pair:Pair {type S = a.A, type T = b.A}):Pair {type S = b.A, type T = a.A}:
+        new this:Pair {type S = b.A, type T = a.A}:
+            type S = b.A
+            type T = a.A
+            val fst = pair.snd
+            val snd = pair.fst
+
+aa.swapPair(IntP, UnitP, p1)
diff --git a/selfhost/tests/subtypeTest.wyv b/selfhost/tests/subtypeTest.wyv
index 09d6d6710..7bf8938e2 100644
--- a/selfhost/tests/subtypeTest.wyv
+++ b/selfhost/tests/subtypeTest.wyv
@@ -1,20 +1,20 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Foo:
+type Foo:z:
     def +(i:Int):Foo
     def -(i:Int):Foo
 subtype Foo extends Int
 
-type A:
+type A:z:
     def calc(x:Int):A
-type B:
+type B:z:
     def calc(x:Int):B
     val z:Int
 subtype B extends A
 subtype B extends Unit
-type C:
+type C:z:
     def calc(x:Int):C
     val z:Int
     val y:B
diff --git a/selfhost/tests/testFn.wyv b/selfhost/tests/testFn.wyv
index 0dd737525..34d5f4eae 100644
--- a/selfhost/tests/testFn.wyv
+++ b/selfhost/tests/testFn.wyv
@@ -1,15 +1,15 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type IntToInt:
+type IntToInt:z:
     def f(i:Int):Int
 
 val succ = new this:IntToInt:
     def f(i:Int):Int:
         i+1
 
-type A:
+type A:z:
     def f(i:IntToInt):Int
 
 val apply0 = new this:A:
diff --git a/selfhost/tests/testInt.wyv b/selfhost/tests/testInt.wyv
index 41f775a42..5fd1bbcfb 100644
--- a/selfhost/tests/testInt.wyv
+++ b/selfhost/tests/testInt.wyv
@@ -1,4 +1,4 @@
-type Int:
+type Int:z:
      def +(i:Int):Int
      def -(i:Int):Int
 
diff --git a/selfhost/tests/testShadow.wyv b/selfhost/tests/testShadow.wyv
index e6a0657e9..3b91fc83e 100644
--- a/selfhost/tests/testShadow.wyv
+++ b/selfhost/tests/testShadow.wyv
@@ -1,21 +1,21 @@
-type Int:
+type Int:z:
      def +(i:Int):Int
      def -(i:Int):Int
 
-type X:
+type X:z:
     val a:Int
 
 val x = new this:X:
     val a = 5
 
-type Fn:
+type Fn:z:
     def f(x:Int):Int
 
 val fn = new this:Fn:
     def f(b:Int):Int:
         x.a + b
 
-type X:
+type X:z:
     val b:Int
 
 val y = new this:X:
diff --git a/selfhost/tests/testVar.wyv b/selfhost/tests/testVar.wyv
index da10c308a..4c4abe714 100644
--- a/selfhost/tests/testVar.wyv
+++ b/selfhost/tests/testVar.wyv
@@ -1,8 +1,8 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type A:
+type A:z:
     val a:Int
 
 val x = new this:A:
diff --git a/selfhost/tests/tree.wyv b/selfhost/tests/tree.wyv
index bea68e0dc..f6e323bd9 100644
--- a/selfhost/tests/tree.wyv
+++ b/selfhost/tests/tree.wyv
@@ -1,15 +1,15 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Tree:
+type Tree:z:
     def sum(u:Unit):Int
 
-type Empty:
+type Empty:z:
     def sum(u:Unit):Int
 subtype Empty extends Tree
 
-type Branch:
+type Branch:z:
     def sum(u:Unit):Int
     val a:Int
     val left:Tree
diff --git a/selfhost/tests/typeTest.wyv b/selfhost/tests/typeTest.wyv
index 60b2dd4b6..f82d4cecc 100644
--- a/selfhost/tests/typeTest.wyv
+++ b/selfhost/tests/typeTest.wyv
@@ -1,23 +1,23 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type Polygon:
+type Polygon:z:
     def perim(u:Unit):Int
 
-type Triangle:
+type Triangle:z:
     val s1:Int
     val s2:Int
     val s3:Int
     def perim(u:Unit):Int
 subtype Triangle extends Polygon
 
-type Square:
+type Square:z:
     val s:Int
     def perim(u:Unit):Int
 subtype Square extends Polygon
 
-type A:
+type A:z:
     def makeTri(a:Int,b:Int,c:Int):Triangle
 
 val a = new this:A:
diff --git a/selfhost/tests/typemember.wyv b/selfhost/tests/typemember.wyv
new file mode 100644
index 000000000..7275f5c41
--- /dev/null
+++ b/selfhost/tests/typemember.wyv
@@ -0,0 +1,23 @@
+type Int:z:
+    def +(i:Int):Int
+    def -(i:Int):Int
+
+type Equatable:z:    
+    type T <= Unit
+    def equals(x:z.T):z.T
+
+type Fruit:z:
+    type T <= Unit
+    type S <= Unit
+    val item:z.T
+    def equals(x:z.T):z.T
+subtype Fruit extends Equatable
+
+val f1 = new this:Fruit {type T = Int}:
+    type T = Int
+    type S = Unit
+    val item:this.T = 3
+    def equals(x:this.T):this.T:
+        this.item + x
+
+f1.equals(3)
diff --git a/selfhost/toBytecode.wyv b/selfhost/toBytecode.wyv
index 4300b3a90..9de0e20e3 100644
--- a/selfhost/toBytecode.wyv
+++ b/selfhost/toBytecode.wyv
@@ -1,6 +1,6 @@
 module def toBytecode(javascript:JavaScript, js:Dyn)
 
-import bound
+import types
 import bytecode
 import wyvern.collections.llist
 import error
@@ -8,35 +8,37 @@ type List = llist.LinkedList
 
 val b = bytecode(javascript, js)
 
-def toBytecode(e:bound.Statement):b.SeqExpr
+def toBytecode(e:types.Statement):b.SeqExpr
     b.SeqExpr(toBytecodeStmt(e))
 
-def toBytecodeStmt(e:bound.Statement):List[b.SeqStmt] = match e:
-    d:bound.DeclStatement => 
+def toBytecodeStmt(e:types.Statement):List[b.SeqStmt] = match e:
+    d:types.DeclStatement => 
         val declBytecode = b.DeclStmt(toBytecodeDecl(d.decl))
         val stmtBytecode = toBytecodeStmt(d.stmt)
         llist.Cons[b.SeqStmt](declBytecode, stmtBytecode)
-    e:bound.ExprStatement => 
+    e:types.ExprStatement => 
         llist.Singleton[b.SeqStmt](b.ExpStmt(toBytecodeExpr(e.exp)))
 
-def toBytecodeDecl(e:bound.Decl):b.Decl = match e:
-    v:bound.Val       => b.ValDecl(v.binding.name, toBytecodeExpr(v.exp))
-    d:bound.Def       => b.MethodDecl(d.binding.name, d.args.map[String](e => e.arg.name), b.SeqExpr(toBytecodeStmt(d.body)))
-    t:bound.TypeDecl  => b.ValDecl("_", toBytecodeExpr(bound.UnitVal()))
-    s:bound.SubtypeDecl => b.ValDecl("_", toBytecodeExpr(bound.UnitVal()))
+def toBytecodeDecl(e:types.Decl):b.Decl = match e:
+    v:types.Val       => b.ValDecl(v.binding.name, toBytecodeExpr(v.exp))
+    d:types.Def       => b.MethodDecl(d.binding.name, d.args.map[String](e => e.name.name), b.SeqExpr(toBytecodeStmt(d.body)))
+    t:types.TypeDecl  => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
+    s:types.SubtypeDecl => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
+    m:types.TypeEq => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
+
 
     default => error.report("not a declaration",error.unknownLocation)
 
-def toBytecodeExpr(e:bound.Exp):b.Expr = match e:
-    v:bound.Var     => b.VarExpr(v.binding.name)
-    c:bound.Call    => b.CallExpr(toBytecodeExpr(c.receiver), c.name, c.args.map[b.Expr](e => toBytecodeExpr(e)), false)
-    f:bound.Field   => b.AccessExpr(toBytecodeExpr(f.receiver), f.field)
+def toBytecodeExpr(e:types.Exp):b.Expr = match e:
+    v:types.Var     => b.VarExpr(v.binding.name)
+    c:types.Call    => b.CallExpr(toBytecodeExpr(c.receiver), c.name, c.args.map[b.Expr](e => toBytecodeExpr(e)), false)
+    f:types.Field   => b.AccessExpr(toBytecodeExpr(f.receiver), f.field)
     // no lambda or app case - should have been lowered away
-    n:bound.New     => b.NewExpr(n.binding.name, n.body.map[b.Decl](d => toBytecodeDecl(d)))
-    i:bound.Integer => b.IntLit(i.str)
-    u:bound.UnitVal => b.IntLit("0")
+    n:types.New     => b.NewExpr(n.binding.name, n.body.map[b.Decl](d => toBytecodeDecl(d)))
+    i:types.Integer => b.IntLit(i.str)
+    u:types.UnitVal => b.IntLit("0")
 
-def writeExpToFile(e:bound.Statement, filename:String):Unit
+def writeExpToFile(e:types.Statement, filename:String):Unit
     js.log("Converting expression to bytecode...\n")
     val expBytecode = toBytecode(e)
     //js.log(d.sequenceExpression.statements.get(0).declaration)
diff --git a/selfhost/typecheck.wyv b/selfhost/typecheck.wyv
index d2118efa4..704633bec 100644
--- a/selfhost/typecheck.wyv
+++ b/selfhost/typecheck.wyv
@@ -1,109 +1,422 @@
 module typecheck
 
 import types
-import subtyping
-import bound
+import typesUtil
 import error
 import wyvern.option
 import wyvern.collections.llist
+import wyvern.pair
+
+type Option = option.Option
 type List = llist.LinkedList
+type Binding = types.Binding
+type Type = types.Type
+type BaseType = types.BaseType
 type DeclType = types.DeclType
-type Option = option.Option
+type ValType = types.ValType
+type TypeType = types.TypeType
+type DefType = types.DefType
+type SubtypeType = types.SubtypeType
+type MemberType = types.MemberType
+type UnitType = types.UnitType
+type NominalType = types.NominalType
+type PathType = types.PathType
+type BotType = types.BotType
+type Pair = pair.Pair
 
-def typecheck(e:bound.Statement):types.Type
+def typecheck(e:types.Statement):Type
     typecheckStmt(e,llist.Nil[DeclType]())
 
-def typecheckStmt(e:bound.Statement, gamma:List[DeclType]):types.Type = match e:
-    d:bound.DeclStatement => 
-        val dc:types.DeclType = typecheckDecl(d.decl, gamma)
+def typecheckStmt(e:types.Statement, gamma:List[DeclType]):Type = match e:
+    d:types.DeclStatement => 
+        val dc:DeclType = typecheckDecl(d.decl, gamma)
         val gammaPrime:List[DeclType] = llist.Cons[DeclType](dc, gamma)
         typecheckStmt(d.stmt, gammaPrime)
-    e:bound.ExprStatement => 
+    e:types.ExprStatement => 
         typecheckExpr(e.exp, gamma)
 
-def typecheckDecl(e:bound.Decl, gamma:List[DeclType]):types.DeclType = match e:
-    v:bound.Val => 
+def typecheckDecl(e:types.Decl, gamma:List[DeclType]):DeclType = match e:
+    v:types.Val => 
         val typ = typecheckExpr(v.exp, gamma)
-        types.ValType(v.binding, typ)
-    t:bound.TypeDecl =>
-        types.TypeType(t.name, t.typ)
-    d:bound.Def =>
-        val argdecls:List[DeclType] = d.args.map[types.ValType]((a:bound.Arg) => types.ValType(a.arg,a.argTyp))
-        val argtypes:List[types.Type] = d.args.map[types.Type]((a:bound.Arg) => a.argTyp)
-        val testType = typecheckStmt(d.body, argdecls.append(gamma))
-        if (subtyping.isSubtype(testType, d.retTyp, gamma))
-            types.DefType(d.binding, argtypes, d.retTyp)
+        if (isSubtype(typ,v.typ,gamma))
+            types.ValType(v.binding, v.typ)
+          else
+            error.report("val expr not a subtype of declared type",error.unknownLocation)
+    t:types.TypeDecl =>
+        val tt = types.TypeType(t.name, t.z, t.typ)
+        val ngamma = llist.Cons[DeclType](types.ValType(t.z,types.makeNominalType(t.name)),gamma)
+        val nngamma = llist.Cons[DeclType](tt,ngamma)
+        if (t.typ.foldRight[Boolean]((x:DeclType,y:Boolean)=>checkDeclTypeWF(x,nngamma),true))
+            tt
           else
-            error.report("def decl is not well-formed",error.unknownLocation)
-    s:bound.SubtypeDecl =>
-        if (subtyping.checkSubtypeWF(s.subtype, s.supertype, gamma))
-            types.SubtypeType(s.subtype, s.supertype)
+            error.report("type decl is not well-formed",error.unknownLocation)
+    d:types.Def =>
+        val ngamma = d.args.map[DeclType](e=>e).append(gamma)
+        val testType = typecheckStmt(d.body, ngamma)
+        if (isSubtype(testType, d.retTyp, ngamma))
+            types.DefType(d.binding, d.args, d.retTyp)
+          else
+            error.report("def decl is not well-formed: " + typesUtil.typeToString(testType) + " is not subtype of " + typesUtil.typeToString(d.retTyp),error.unknownLocation)
+    s:types.SubtypeDecl =>
+        val subDecl = types.SubtypeType(s.subtype, s.supertype)
+        if (checkDeclTypeWF(subDecl, gamma))
+            subDecl
           else
             error.report("subtype decl is not well-formed",error.unknownLocation)
+    t:types.TypeEq =>
+        if (checkTypeWF(t.typ,gamma))
+            types.MemberType(t.name, types.EQ(),t.typ)
+          else
+            error.report("typeEq type not well-formed",error.unknownLocation)
 
-def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
-    v:bound.Var =>
+def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e:
+    v:types.Var =>
         val pred = ((b:DeclType) => 
             val z = match b:
-                va:types.ValType => 
-                    if (types.equalBinding(v.binding,va.name)) { option.Some[types.ValType](va) } else { option.None[types.ValType]() }
-                default => option.None[types.ValType]()
+                va:ValType => 
+                    if (types.equalBinding(v.binding,va.name)) { option.Some[ValType](va) } else { option.None[ValType]() }
+                default => option.None[ValType]()
             z
         )
-        types.findInDeclList[types.ValType](gamma, pred).typ
+        typesUtil.findInDeclList[ValType](gamma, pred).typ
 
-    c:bound.Call => //T-Invk
+    c:types.Call => //T-Invk
         val recType = typecheckExpr(c.receiver, gamma)
-        val unfold = types.unfoldType(recType, gamma)
-        val argtypes:List[types.Type] = c.args.map[types.Type](e => typecheckExpr(e,gamma))
+        val unfold = unfoldType(recType, gamma)
+        val argtypes:List[Type] = c.args.map[Type](e => typecheckExpr(e,gamma))
 
-        val subcheck = x:types.Type => y:types.Type => subtyping.isSubtype(x,y,gamma)
         val pred = ((b:DeclType) =>
             val z = match b:
-                da:types.DefType => 
-                    if (c.name == da.name.name && subtyping.checkArgList(argtypes,da.args,subcheck)) { option.Some[types.DefType](da) } else { option.None[types.DefType]() }
-                default => option.None[types.DefType]()
+                da:DefType => 
+                    val argBindings = da.args.map[Binding](a => a.name)
+
+                    val argsSub = da.args.map[ValType](e => types.ValType(e.name,types.substituteType(e.typ,c.receiver,unfold.z)))
+                    val argsSub2 = argsSub.map[ValType](e => types.ValType(e.name,typesUtil.doListOfSubstitutions(e.typ,c.args,argBindings)))
+                    val defargs = argsSub2.map[Type](e => e.typ)
+
+                    val ngamma:List[DeclType] = argsSub2.map[DeclType](e => e).append(gamma)
+
+                    val subcheck = x:Type => y:Type => isSubtype(x,y,ngamma)
+                    if (c.name == da.name.name && checkArgList(argtypes,defargs,subcheck)) { option.Some[DefType](da) } else { option.None[DefType]() }
+                default => option.None[DefType]()
             z
         )
-        types.findInDeclList[types.DefType](unfold, pred).retTyp
+        val func = typesUtil.findInDeclList[DefType](unfold.decls, pred)
+        //Do substitutions to get the correct return type
+        val retTyp = types.substituteType(func.retTyp, c.receiver, unfold.z)
+        val argBindings = func.args.map[Binding](a => a.name)
+        typesUtil.doListOfSubstitutions(retTyp,c.args,argBindings)
 
-    f:bound.Field => //T-Field
+    f:types.Field => //T-Field
         val recType = typecheckExpr(f.receiver, gamma)
-        val unfold = types.unfoldType(recType, gamma)
+        val unfold = unfoldType(recType, gamma)
         val pred = ((b:DeclType) =>
             val z = match b:
-                va:types.ValType => 
-                    if (f.field == va.name.name) { option.Some[types.ValType](va) } else { option.None[types.ValType]() }
-                default => option.None[types.ValType]()
+                va:ValType => 
+                    if (f.field == va.name.name) { option.Some[ValType](va) } else { option.None[ValType]() }
+                default => option.None[ValType]()
             z
         )
-        types.findInDeclList[types.ValType](unfold, pred).typ
+        val tauV = typesUtil.findInDeclList[ValType](unfold.decls, pred).typ
+        types.substituteType(tauV, f.receiver, unfold.z)
+
+    n:types.New => //T-New
+        val unfold = unfoldType(n.typ, gamma)
 
-    n:bound.New => //T-New
-        val unfold = types.unfoldType(n.typ, gamma)
-        def typeNewDecls(d:bound.Decl):DeclType
-            val thisType = types.ValType(n.binding, n.typ)
-            val ngamma = llist.Cons[DeclType](thisType, gamma)
+        val thisType = types.ValType(n.binding, n.typ)
+        val ngamma = llist.Cons[DeclType](thisType, gamma)
+        def typeNewDecls(d:types.Decl):DeclType
             match d:
-                v:bound.Val       => typecheckDecl(d, gamma)
-                d:bound.Def       => typecheckDecl(d, ngamma)
-                t:bound.TypeDecl  => typecheckDecl(d, ngamma)
+                v:types.Val         => typecheckDecl(d, ngamma)
+                d:types.Def         => typecheckDecl(d, ngamma)
+                t:types.TypeDecl    => typecheckDecl(d, ngamma)
+                s:types.SubtypeDecl => typecheckDecl(d, ngamma)
+                t:types.TypeEq      => typecheckDecl(d, ngamma)
         val decls = n.body.map[DeclType](x => typeNewDecls(x))
-        if (subtyping.checkDeclList(decls, unfold, x=>y=>subtyping.isSubtypeDecl(x,y,gamma)))
-            n.typ
-          else
-            error.report("invalid new expression",error.unknownLocation)
+        val unfoldDecls = unfold.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(n.binding),unfold.z))
+        if (isSubtypeDeclList(decls,unfoldDecls,ngamma)) 
+            n.typ 
+          else 
+            error.report("invalid new expression: "+"decls:\n" + typesUtil.combineWithNewlines(unfoldDecls.map[String](e => typesUtil.declTypeToString(e))),error.unknownLocation)
 
-    i:bound.Integer => 
+    i:types.Integer => 
         val pred = ((b:DeclType) =>
             val z = match b:
-                tt:types.TypeType => 
-                    if (tt.name.name == "Int") { option.Some[types.TypeType](tt) } else { option.None[types.TypeType]() }
-                default => option.None[types.TypeType]()
+                tt:TypeType => 
+                    if (tt.name.name == "Int") { option.Some[TypeType](tt) } else { option.None[TypeType]() }
+                default => option.None[TypeType]()
             z
         ) 
-        types.makeNominalType(types.findInDeclList[types.TypeType](gamma, pred).name)
+        val L = typesUtil.findInDeclList[TypeType](gamma, pred).name
+        types.makeNominalType(L)
 
-    u:bound.UnitVal => types.theUnit
+    u:types.UnitVal => types.theUnit
 
     default => error.report("type error: unrecognized expression",error.unknownLocation)
+/////////////////////////////////
+//UNFOLD
+type Unfold
+    val z:Binding
+    val decls:List[DeclType]
+def Unfold(z:Binding, decls:List[DeclType]):Unfold = new
+    val z = z
+    val decls = decls
+
+def fetchDeclFromList(path:PathType, ls:List[DeclType]):DeclType
+    val pred = ((d:DeclType) => 
+        val z = match d:
+            t:TypeType   => path.t == t.name.name 
+            m:MemberType => path.t == m.name.name
+            default => false
+        z
+    )
+    val search = llist.find[DeclType](ls,pred)
+    match search:
+        s:option.Some => s.get()
+        default => error.report("fetch: type member not found",error.unknownLocation)
+
+def unfoldType(x:Type, gamma:List[DeclType]):Unfold
+    val b = match x.base:
+        u:UnitType => 
+            val pred = typesUtil.findTypePredicateFromStr("Unit")
+            val tt = typesUtil.findInDeclList[TypeType](gamma, pred)
+            Unfold(tt.z,llist.Nil[DeclType]())
+        x:NominalType => 
+            val pred = typesUtil.findTypePredicate(x.L)
+            val tt = typesUtil.findInDeclList[TypeType](gamma, pred)
+            Unfold(tt.z,tt.unfld)
+        path:PathType =>
+                val tau = typecheckExpr(path.p,gamma)
+                val pUnfold = unfoldType(tau,gamma)
+                val d = fetchDeclFromList(path,pUnfold.decls)
+                match d:
+                    t:TypeType => 
+                        val subUnfold = t.unfld.map[DeclType](e => types.substituteDeclType(e,path.p,pUnfold.z))
+                        Unfold(t.z,subUnfold)
+                    m:MemberType => match m.bound:
+                        g:types.GEQ => 
+                            val pred = typesUtil.findTypePredicateFromStr("Unit")
+                            val tt = typesUtil.findInDeclList[TypeType](gamma, pred)
+                            Unfold(tt.z,llist.Nil[DeclType]())
+                        default => unfoldType(types.substituteType(m.typ,path.p,pUnfold.z),gamma)
+                    default => error.report("should never happend",error.unknownLocation)
+    Unfold(b.z,typesUtil.mergeDeclList(x.refines,b.decls))
+/////////////////////////////////
+//SUBTYPING
+
+//Check if two lists of arguments line up in the right way
+def checkArgList(xs:List[Type],ys:List[Type],pred:Type->Type->Boolean):Boolean
+    if (xs.size() == ys.size())
+        def f(xs:List[Type],ys:List[Type]):Boolean = match xs:
+            a:llist.Cons => match ys:
+                b:llist.Cons =>   
+                    (pred(a.value)(b.value)) && f(a.next,b.next)
+            default => true
+        f(xs,ys)
+      else
+        false
+
+//Check if for each y in ys there is an x in xs s.t. (pred x y) is true
+def checkDeclList(xs:List[DeclType],ys:List[DeclType],pred:DeclType->DeclType->Boolean):Boolean
+    def isValid(d:DeclType):Boolean
+        val search = llist.find[DeclType](xs, (e:DeclType) => pred(e)(d))
+        match search:
+            s:option.Some => true
+            default => false
+    ys.foldRight[Boolean]((x:DeclType,y:Boolean) => isValid(x) && y, true)
+
+def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
+    v:ValType => match b:
+        u:ValType => v.name.name == u.name.name && equalType(v.typ,u.typ,gamma)
+        default => false
+    t:TypeType => match b:
+        u:TypeType => 
+            t.name.name == u.name.name && checkDeclList(t.unfld,u.unfld,x=>y=>equalDeclType(x,y,gamma))
+        default => false
+    d:DefType => match b:
+        u:DefType => 
+            val dargs = d.args.map[Type](e => e.typ)
+            val uargs = u.args.map[Type](e => e.typ)
+            val ngamma = d.args.map[DeclType](e=>e).append(gamma)
+            val nngamma = u.args.map[DeclType](e=>e).append(ngamma)
+            val pred = x:Type => y:Type => equalType(x,y,nngamma)
+            d.name.name == u.name.name && checkArgList(dargs,uargs,pred) && equalType(d.retTyp,u.retTyp,nngamma)
+        default => false
+    s:SubtypeType => match b:
+        u:SubtypeType =>
+            equalType(s.subtype,u.subtype,gamma) && equalType(s.supertype,u.supertype,gamma)            
+        default => false
+    m:MemberType => match b:
+        u:MemberType =>
+            m.name.name == u.name.name && typesUtil.equalBound(m.bound,u.bound) && equalType(m.typ,u.typ,gamma)
+        default => false
+
+def equalBaseType(a:BaseType, b:BaseType, gamma:List[DeclType]):Boolean = match a:
+    u:UnitType => match b:
+        v:UnitType => true
+        default => false
+    bot:BotType => match b:
+        v:BotType => true
+        default => false
+    n:NominalType => match b:
+        v:NominalType => types.equalBinding(n.L,v.L)
+        default => false
+    path:PathType => match b:
+        v:PathType => 
+            val tauA = typecheckExpr(path.p,gamma)
+            val tauB = typecheckExpr(v.p,gamma)
+            (typesUtil.equalPath(path.p,v.p) || equalType(tauA,tauB,gamma)) && path.t == v.t
+        default => false
+
+def equalType(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
+    val pred = x:DeclType => y:DeclType => equalDeclType(x,y,gamma)
+    equalBaseType(t1.base,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,pred) && checkDeclList(t2.refines,t1.refines,pred)
+
+def isSubtypeDeclList(xs:List[DeclType], ys:List[DeclType], gamma:List[DeclType]):Boolean
+    checkDeclList(xs,ys,x=>y=>isSubtypeDecl(x,y,gamma))
+
+def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
+    v:ValType => match b:    
+        u:ValType => v.name.name == u.name.name && isSubtype(v.typ,u.typ,gamma)
+        default => false
+    t:TypeType => match b:
+        u:TypeType => equalDeclType(a,b,gamma)
+        default => false
+    d:DefType => match b:
+        u:DefType => 
+            val dargs = d.args.map[Type](e => e.typ)
+            val uargs = u.args.map[Type](e => e.typ)
+            val ngamma = d.args.map[DeclType](e=>e).append(gamma)
+            val nngamma = u.args.map[DeclType](e=>e).append(ngamma)
+            val pred = x:Type => y:Type => isSubtype(x,y,nngamma)
+            d.name.name == u.name.name && checkArgList(uargs,dargs,pred) && isSubtype(d.retTyp,u.retTyp,nngamma)
+        default => false
+    s:SubtypeType => match b:
+        u:SubtypeType => equalType(s.subtype,u.subtype,gamma)
+        default => false
+    m:MemberType => match b:
+        //RHS =: LHS =
+        //RHS <=: LHS <=, =
+        //RHS >=: LHS >=, =
+        u:MemberType => 
+            if (m.name.name == u.name.name)
+                match u.bound:
+                    e:types.EQ => match m.bound:
+                        ee:types.EQ => 
+                            equalType(m.typ,u.typ,gamma) || (isSubtype(m.typ,u.typ,gamma) && isSubtype(u.typ,m.typ,gamma))
+                        default => false
+                    l:types.LEQ => match m.bound:
+                        g:types.GEQ => false
+                        default => isSubtype(m.typ,u.typ,gamma)
+                    g:types.GEQ => match m.bound:
+                        l:types.LEQ => false
+                        default => isSubtype(u.typ,m.typ,gamma)
+              else
+                false
+        default => false
+
+def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
+    def normalAns():Boolean
+        if (equalType(t2,types.theUnit,gamma)) 
+            true 
+          else 
+            match t1.base:
+                b:BotType => true
+                default => 
+                    if (isSubtypeBase(t1,t2.base,gamma)) 
+                        val unfold = unfoldType(t1,gamma)
+                        val ngamma = llist.Cons[DeclType](types.ValType(unfold.z,t1),gamma)
+                        isSubtypeDeclList(unfold.decls,t2.refines,ngamma)
+                      else
+                        false
+    def recurseRHS():Boolean = match t2.base:
+        path:PathType =>
+            val tau = typecheckExpr(path.p,gamma)
+            val pUnfold = unfoldType(tau,gamma)
+            val d = fetchDeclFromList(path,pUnfold.decls)
+            match d:
+                m:MemberType => match m.bound:
+                    l:types.LEQ => false
+                    default =>
+                        val typeBound = typesUtil.addRefines(m.typ,t2.refines)
+                        val subType = types.substituteType(typeBound,path.p,pUnfold.z)
+                        isSubtype(t1,subType,gamma)
+                t:TypeType => false
+        default => false
+
+    def recurseLHS():Boolean = match t1.base:
+        path:PathType =>
+            val tau = typecheckExpr(path.p,gamma)
+            val pUnfold = unfoldType(tau,gamma)
+            val d = fetchDeclFromList(path,pUnfold.decls)
+            match d:
+                m:MemberType => match m.bound:
+                    l:types.GEQ => false
+                    default =>
+                        val typeBound = typesUtil.addRefines(m.typ,t1.refines)
+                        val subType = types.substituteType(typeBound,path.p,pUnfold.z)
+                        isSubtype(subType,t2,gamma)
+                t:TypeType => false
+        default => false
+    
+    if (equalBaseType(t1.base,t2.base,gamma))
+        isSubtypeDeclList(t1.refines,t2.refines,gamma)
+      else
+        //try both left and right bounds at the same time
+        recurseLHS() || recurseRHS() || normalAns()
+
+def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
+    if (equalBaseType(t1.base,t2,gamma))
+        true
+      else
+        val pred = ((b:DeclType) =>
+            val z = match b:
+                s:types.SubtypeType =>
+                    equalBaseType(s.subtype.base,t1.base,gamma) \
+                 && isSubtypeDeclList(t1.refines,s.subtype.refines,gamma) \
+                 && isSubtypeBase(types.Type(s.supertype.base,t1.refines),t2,gamma)
+                default => false
+            z
+        )
+        val listToSearch:List[DeclType] = match t1.base:
+            path:PathType => 
+                val tau = typecheckExpr(path.p,gamma)
+                val unfold = unfoldType(tau,gamma)
+                unfold.decls.map[DeclType](d => types.substituteDeclType(d,path.p,unfold.z))
+            default => gamma
+        val search = llist.find[DeclType](listToSearch,pred)
+        match search:
+            s:option.Some => true
+            default => false
+
+def checkTypeWF(t:Type, gamma:List[DeclType]):Boolean
+    match t.refines:
+        n:llist.Nil => true
+        c:llist.Cons =>
+            val ua = unfoldType(t,gamma)
+            val ub = unfoldType(types.Type(t.base,llist.Nil[DeclType]()),gamma)
+            val ngamma = llist.Cons[DeclType](types.ValType(ua.z,t),gamma)
+            isSubtypeDeclList(ua.decls,ub.decls,ngamma)
+    
+def checkDeclTypeWF(decl:DeclType,gamma:List[DeclType]):Boolean
+    match decl:
+        v:ValType     => checkTypeWF(v.typ,gamma)
+        t:TypeType    =>
+            val ngamma = llist.Cons[DeclType](types.ValType(t.z,types.makeNominalType(t.name)),gamma)
+            val nngamma = llist.Cons[DeclType](t,ngamma)
+            t.unfld.foldRight[Boolean]((d:DeclType,y:Boolean)=>checkDeclTypeWF(d,nngamma) && y,true)
+        d:DefType     =>
+            val ngamma = d.args.map[DeclType](e=>e).append(gamma)
+            val checkArgsWF = d.args.foldRight[Boolean]((v:ValType,y:Boolean)=>checkTypeWF(v.typ,ngamma) && y,true)
+            val checkRetWF = checkTypeWF(d.retTyp,ngamma)
+            checkArgsWF && checkRetWF
+        s:SubtypeType =>
+            val t1 = s.subtype
+            val t2 = s.supertype
+            val ua = unfoldType(t1,gamma)
+            val ub = unfoldType(t2,gamma)
+            val ngamma = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma)
+            val nngamma = llist.Cons[DeclType](types.ValType(ua.z,t1),ngamma)
+            val supertypeDecls = ub.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(ua.z),ub.z))
+            isSubtypeDeclList(ua.decls,supertypeDecls,nngamma)
+        m:MemberType  => checkTypeWF(m.typ,gamma)
diff --git a/selfhost/types.wyv b/selfhost/types.wyv
index 56a0404e4..0e3f94253 100644
--- a/selfhost/types.wyv
+++ b/selfhost/types.wyv
@@ -1,11 +1,14 @@
 module types
 
+import raw
 import wyvern.option
 import wyvern.collections.llist
 import error
 type Option = option.Option
 type List = llist.LinkedList
 
+//////////////////////////////
+//Binding defn
 resource type Counter
     var value:Int
 def Counter():Counter = new
@@ -24,9 +27,51 @@ def Binding(name:String, c:Counter):Binding
 def equalBinding(b1:Binding, b2:Binding):Boolean
     b1.name == b2.name && b1.id == b2.id
 //////////////////////////////
+//bound AST defn
+resource type Context
+    val bindings:List[DeclType]
+    val counter:Counter
+    val parse:String -> raw.Exp
+    def extend(b:DeclType):Context
+    def extendList(b:List[DeclType]):Context
+
+def Context(bs:List[DeclType], c:Counter, p:String -> raw.Exp) : Context = new
+    val bindings = bs
+    val counter = c
+    val parse = p
+    def extend(b:DeclType):Context
+        Context(llist.Cons[DeclType](b, bs), c, p)
+    def extendList(b:List[DeclType]):Context
+        val newBindings = b.append(bs)
+        Context(newBindings,c,p)
+    
+def emptyContext(p:String -> raw.Exp):Context = Context(llist.Nil[DeclType](), Counter(), p)
+
+datatype Statement
+    DeclStatement(decl:Decl, stmt:Statement)
+    ExprStatement(exp:Exp)
+
+datatype Decl
+    Val(binding:Binding, typ:Type, exp:Exp)
+    Def(binding:Binding, args:List[ValType], retTyp:Type, body:Statement)
+    TypeDecl(name:Binding, z:Binding, typ:List[DeclType])
+    SubtypeDecl(subtype:Type, supertype:Type)
+    TypeEq(name:Binding, typ:Type)
+
+datatype Exp
+    Var(binding:Binding)
+    Call(receiver:Exp, name:String, args:List[Exp])
+    Field(receiver:Exp, field:String)
+    New(binding:Binding, typ:Type, body:List[Decl])
+    Integer(str:String)
+    UnitVal()
+//////////////////////////////
+//Type defn
 datatype BaseType
     UnitType()
+    BotType()
     NominalType(L:Binding)
+    PathType(p:Exp, t:String)
 
 type Type
     val base:BaseType
@@ -40,63 +85,38 @@ def makeNominalType(L:Binding):Type = new
 def makeRefines(ls:List[DeclType]):Type = new
     val base = UnitType()
     val refines = ls
-def makeBase(b:BaseType):Type
-    Type(b,llist.Nil[DeclType]())
+
+datatype Bound
+    LEQ()    
+    EQ()
+    GEQ()
 
 datatype DeclType
     ValType(name:Binding, typ:Type)
-    TypeType(name:Binding, unfld:Type)
-    DefType(name:Binding, args:List[Type], retTyp:Type)
+    TypeType(name:Binding, z:Binding, unfld:List[DeclType])
+    DefType(name:Binding, args:List[ValType], retTyp:Type)
     SubtypeType(subtype:Type, supertype:Type)
+    MemberType(name:Binding, bound:Bound, typ:Type)
 
 val theUnit = Type(UnitType(),llist.Nil[DeclType]())
 //////////////////////////////
-def findInDeclList[T](gamma:List[DeclType], pred:DeclType->Option[T]):T
-    def f(gamma:List[DeclType], pred:DeclType->Option[T]):Option[T]
-        match gamma:
-            c:llist.Cons => 
-                match (pred(c.value)):
-                    s:option.Some => s
-                    default => f(c.next, pred)
-            n:llist.Nil => option.None[T]()
-    match f(gamma, pred):
-        s:option.Some => s.get()
-        default => error.report("search in decllist failed",error.unknownLocation)
-
-def findTypePredicate(bind:Binding):DeclType->Option[TypeType]
-    val pred = ((b:DeclType) =>
-        val z = match b:
-            t:TypeType => if (equalBinding(bind, t.name)) { option.Some[TypeType](t) } else { option.None[TypeType]() }
-            default => option.None[TypeType]()
-        z
-    )
-    pred
-
-def unfoldType(x:Type, gamma:List[DeclType]):List[DeclType]
-    val decls = match x.base:
-        u:UnitType => llist.Nil[DeclType]()
-        x:NominalType => 
-            val pred = findTypePredicate(x.L)
-            unfoldType(findInDeclList[TypeType](gamma, pred).unfld,gamma)
-    x.refines.append(decls)
-
-def combineStringList(ls:List[String]):String = match ls:
-    c:llist.Cons => match c.next:
-        n:llist.Nil => c.value
-        cc:llist.Cons => c.value + ", " + combineStringList(c.next)
-    default => ""
+def substituteBaseType(beta:BaseType, newb:Exp, oldb:Binding):BaseType = match beta:
+    p:PathType => PathType(substituteExp(p.p,newb,oldb),p.t)
+    default => beta
+        
+def substituteType(tau:Type, newb:Exp, oldb:Binding):Type
+    val subBase = substituteBaseType(tau.base,newb,oldb)
+    val subRefines = tau.refines.map[DeclType](e => substituteDeclType(e,newb,oldb))
+    Type(subBase,subRefines)
 
-def declTypeToString(d:DeclType):String = match d:
-    v:ValType => "val " + v.name.name + ":" + typeToString(v.typ)
-    t:TypeType => "type " + t.name.name + ":" + typeToString(t.unfld)
-    d:DefType => 
-        val arglist = d.args.map[String](t => typeToString(t))
-        "def " + d.name.name + "(" + combineStringList(arglist) + "):" + typeToString(d.retTyp)
+def substituteDeclType(d:DeclType, newb:Exp, oldb:Binding):DeclType = match d:
+    v:ValType     => ValType(v.name,substituteType(v.typ,newb,oldb))
+    t:TypeType    => TypeType(t.name,t.z,t.unfld.map[DeclType](e => substituteDeclType(e,newb,oldb)))
+    d:DefType     => DefType(d.name,d.args.map[ValType](e=>ValType(e.name,substituteType(e.typ,newb,oldb))),substituteType(d.retTyp,newb,oldb))
+    s:SubtypeType => SubtypeType(substituteType(s.subtype,newb,oldb),substituteType(s.supertype,newb,oldb))
+    m:MemberType  => MemberType(m.name,m.bound,substituteType(m.typ,newb,oldb))
 
-def typeToString(t:Type):String
-    val baseString = match t.base:
-        u:UnitType => "Unit"
-        n:NominalType => n.L.name
-    val s = t.refines.map[String](e => declTypeToString(e))
-    val refinesString = combineStringList(s)
-    baseString + " {" + refinesString + "}"
+def substituteExp(e:Exp, newb:Exp, oldb:Binding):Exp = match e:
+    v:Var => if (equalBinding(v.binding, oldb)) { newb } else { v }
+    f:Field => Field(substituteExp(f.receiver,newb,oldb),f.field)
+    default => error.report("Substitution into invalid path type",error.unknownLocation)
diff --git a/selfhost/typesUtil.wyv b/selfhost/typesUtil.wyv
new file mode 100644
index 000000000..566055fbd
--- /dev/null
+++ b/selfhost/typesUtil.wyv
@@ -0,0 +1,164 @@
+module typesUtil
+
+import wyvern.option
+import wyvern.collections.llist
+import wyvern.pair
+import error
+import types
+type Option = option.Option
+type List = llist.LinkedList
+type Binding = types.Binding
+type Type = types.Type
+type DeclType = types.DeclType
+type BaseType = types.BaseType
+type ValType = types.ValType
+type TypeType = types.TypeType
+type DefType = types.DefType
+type SubtypeType = types.SubtypeType
+type MemberType = types.MemberType
+type UnitType = types.UnitType
+type BotType = types.BotType
+type NominalType = types.NominalType
+type PathType = types.PathType
+type Pair = pair.Pair
+
+def findInDeclList[T](gamma:List[DeclType], pred:DeclType->Option[T]):T
+    def f(gamma:List[DeclType], pred:DeclType->Option[T]):Option[T]
+        match gamma:
+            c:llist.Cons => 
+                match (pred(c.value)):
+                    s:option.Some => s
+                    default => f(c.next, pred)
+            n:llist.Nil => option.None[T]()
+    match f(gamma, pred):
+        s:option.Some => s.get()
+        default => error.report("search in decllist failed",error.unknownLocation)
+
+def zip[U,T](xs:List[U], ys:List[T]):List[Pair[U,T]] = match xs:
+    c:llist.Cons => match ys:
+        cc:llist.Cons => llist.Cons[Pair[U,T]](pair.Pair[U,T](c.value,cc.value), zip[U,T](c.next,cc.next))
+        default => llist.Nil[Pair[U,T]]()
+    default => llist.Nil[Pair[U,T]]()
+
+def doListOfSubstitutions(ty:Type, exps:List[types.Exp], bindings:List[Binding]):Type
+    val zipargs = zip[types.Exp,Binding](exps,bindings)
+    zipargs.foldRight[Type]((x:Pair[types.Exp,Binding],t:Type)=>types.substituteType(t,x.first,x.second),ty)
+
+def equalBound(a:types.Bound, b:types.Bound):Boolean = match a:
+    x:types.LEQ => match b:
+        y:types.LEQ => true   
+        default => false
+    x:types.EQ => match b:
+        y:types.EQ => true   
+        default => false
+    x:types.GEQ => match b:
+        y:types.GEQ => true   
+        default => false
+
+def equalPath(p1:types.Exp, p2:types.Exp):Boolean = match p1:
+    v:types.Var => match p2:
+        u:types.Var => types.equalBinding(v.binding,u.binding)
+        default => false
+    v:types.Field => match p2:
+        u:types.Field => equalPath(v.receiver,u.receiver) && v.field == u.field
+        default => false
+    default => false
+
+def addRefines(t:Type, decls:List[DeclType]):Type
+    types.Type(t.base,decls.append(t.refines))
+
+def findTypePredicate(bind:Binding):DeclType->Option[TypeType]
+    val pred = ((b:DeclType) =>
+        val z = match b:
+            t:TypeType => if (types.equalBinding(bind, t.name)) { option.Some[TypeType](t) } else { option.None[TypeType]() }
+            default => option.None[TypeType]()
+        z
+    )
+    pred
+
+def findTypePredicateFromStr(s:String):DeclType->Option[TypeType]
+    val pred = ((d:DeclType) =>
+        val z = match d:
+            tt:types.TypeType =>
+                if (tt.name.name == s) { option.Some[types.TypeType](tt) } else { option.None[types.TypeType]() }
+            default => option.None[types.TypeType]()
+        z
+    )
+    pred
+
+def isMatchDeclType(a:DeclType, b:DeclType):Boolean = match a:
+    v:ValType => match b:    
+        u:ValType => v.name.name == u.name.name
+        default => false
+    t:TypeType => match b:
+        u:TypeType => t.name.name == u.name.name
+        default => false
+    d:DefType => match b:
+        u:DefType => d.name.name == u.name.name
+        default => false
+    s:SubtypeType => false
+    m:MemberType => match b:
+        u:MemberType => m.name.name == u.name.name
+        default => false
+
+//delete replaced ones in ys
+def mergeDeclList(xs:List[DeclType], ys:List[DeclType]):List[DeclType]
+    val pred = ((b:DeclType) =>
+        val search = llist.find[DeclType](xs, (e:DeclType) => isMatchDeclType(e,b))
+        val ans = match search:
+            s:option.Some => false
+            default => true
+        ans
+    )
+    xs.append(ys.filter(pred))
+    
+/////////////////////////
+def printDeclList(ls:List[DeclType]):String
+    combineWithNewlines(ls.map[String](e => declTypeToString(e)))
+def combineWithNewlines(ls:List[String]):String = match ls:
+    c:llist.Cons => match c.next:
+        n:llist.Nil => c.value
+        cc:llist.Cons => c.value + "\n" + combineWithNewlines(c.next)
+    default => ""
+
+def combineStringList(ls:List[String]):String = match ls:
+    c:llist.Cons => match c.next:
+        n:llist.Nil => c.value
+        cc:llist.Cons => c.value + ", " + combineStringList(c.next)
+    default => ""
+
+def declTypeToString(d:DeclType):String = match d:
+    v:ValType => "val " + v.name.name + ":" + typeToString(v.typ)
+    t:TypeType => 
+        val s = t.unfld.map[String](e => declTypeToString(e))
+        "type " + t.name.name + ":" + " {" + combineStringList(s) + "}"
+    d:DefType => 
+        val arglist = d.args.map[String](t => t.name.name + ":" + typeToString(t.typ))
+        "def " + d.name.name + "(" + combineStringList(arglist) + "):" + typeToString(d.retTyp)
+    s:SubtypeType => "subtype " + typeToString(s.subtype) + " extends " + typeToString(s.supertype)
+    m:MemberType => 
+        val boundStr:String = match m.bound:
+            a:types.LEQ => " <= "
+            a:types.EQ  => " = "
+            a:types.GEQ => " >= "
+        "type " + m.name.name + boundStr + typeToString(m.typ)
+
+def typeToString(t:Type):String
+    val baseString = match t.base:
+        u:UnitType => "Unit"
+        b:BotType => "Bottom"
+        n:NominalType => n.L.name
+        path:PathType => expToString(path.p) + "." + path.t
+    val s = t.refines.map[String](e => declTypeToString(e))
+    val refinesString = combineStringList(s)
+    baseString + " {" + refinesString + "}"
+
+def expToString(e:types.Exp):String = match e:
+    v:types.Var  => v.binding.name
+    c:types.Call => 
+        val argList = c.args.map[String](e => expToString(e))
+        expToString(c.receiver) + "." + c.name + "(" + combineStringList(argList) + ")"
+    f:types.Field   => expToString(f.receiver) + "." + f.field
+    n:types.New     => "new"
+    i:types.Integer => i.str
+    u:types.UnitVal => "()"
diff --git a/selfhost/wyvernLexer.wyv b/selfhost/wyvernLexer.wyv
index c89546ba5..385c5b5c0 100644
--- a/selfhost/wyvernLexer.wyv
+++ b/selfhost/wyvernLexer.wyv
@@ -41,10 +41,14 @@ val lowLevelLexer : lexing.Lexer = ~
         rparen:     ')',
         lbrack:     '[',
         rbrack:     ']',
+        lcurl:      '{',
+        rcurl:      '}',
         darrow:     '=>',
         arrow:      '->',
         colon:      ':',
         eq:         '=',
+        leq:        '<=',
+        geq:        '>=',
         dot:        '.',
         comma:      ',',
         linecont:   '\\',
@@ -216,7 +220,7 @@ def makeSecondLevelLexer():SecondLevelLexer = new (self) =>
     def handleLine(pending_:List[Dyn], tokens:List[Token]):List[Dyn]
         //inLine = true
         var toks:List[Dyn] = tokens
-        printTokens(toks)
+        //printTokens(toks)
         var pending:List[Dyn] = pending_ // in reverse order
         
         def computeDedents(matchingType:String):Unit
@@ -276,9 +280,9 @@ def makeSecondLevelLexer():SecondLevelLexer = new (self) =>
     def lexLines(input:String):List[Dyn]
         val lineMatch = regexUtils.doMatch(input, "[^\\r\\n]*")
         if (lineMatch.found)
-            js.log("reading line \"" + lineMatch.matched + "\"")
+            //js.log("reading line \"" + lineMatch.matched + "\"")
             val firstTokens = self.lexLine(lineMatch.matched)
-            printTokens(firstTokens)
+            //printTokens(firstTokens)
             if (lineMatch.after == "")
                 def getBlocks():List[Dyn]
                     val topState = self.lexerState.nth(0).getOrElse(() => DontCare())
@@ -331,9 +335,9 @@ def initLexer(toks : List[Dyn]):lexing.Lexer
                            //js.log("lexer returning " + token.value)
                            c.value
             n:llist.Nil => js.getUndefined()
-        def save():Dyn = js.log("called save\n")
+        def save():Dyn = unit //js.log("called save\n")
         def reset(chunk:String, info:Dyn):Unit
-            js.log("called reset\n")
+            //js.log("called reset\n")
             val secondLevelLexer = makeSecondLevelLexer()
             tokens = secondLevelLexer.lexLines(chunk).filter((t:Dyn) => !js.equalsJS("WS", t."type"))
             //tokens.do((t:Dyn) => printToken(t))
diff --git a/selfhost/wyvernParser.wyv b/selfhost/wyvernParser.wyv
index 6c8b88568..cf527b317 100644
--- a/selfhost/wyvernParser.wyv
+++ b/selfhost/wyvernParser.wyv
@@ -20,8 +20,10 @@ val grammar: parsing.Grammar = ~
            | %val %identifier %eq Expression                          : a:Dyn => raw.Val(a.get(1).value, a.get(3))
            | %val %identifier %colon Type %eq Expression              : a:Dyn => raw.ValAnnot(a.get(1).value, a.get(3), a.get(5))
            | %def %identifier %lparen Arguments %rparen %colon Type %colon %block : a:Dyn => raw.Def(a.get(1).value, a.get(3), a.get(6), a.get(8).value)
-           | %type %identifier %colon %block                          : a:Dyn => raw.TypeDecl(a.get(1).value, a.get(3).value)
-           | %type %identifier %eq %identifier                        : a:Dyn => raw.TypeAlias(a.get(1).value, a.get(3).value)
+           | %type %identifier %colon %identifier %colon %block       : a:Dyn => raw.TypeDecl(a.get(1).value, a.get(3).value, a.get(5).value)
+           | %type %identifier %eq Type                               : a:Dyn => raw.TypeMem(a.get(1).value, raw.EQ(), a.get(3))
+           | %type %identifier %leq Type                              : a:Dyn => raw.TypeMem(a.get(1).value, raw.LEQ(), a.get(3))
+           | %type %identifier %geq Type                              : a:Dyn => raw.TypeMem(a.get(1).value, raw.GEQ(), a.get(3))
            | %val %identifier %colon Type                             : a:Dyn => raw.ValType(a.get(1).value, a.get(3))
            | %def %identifier %lparen Arguments %rparen %colon Type   : a:Dyn => raw.DefDecl(a.get(1).value, a.get(3), a.get(6))
            | %def %plus %lparen Arguments %rparen %colon Type         : a:Dyn => raw.DefDecl("+", a.get(3), a.get(6))
@@ -33,7 +35,14 @@ val grammar: parsing.Grammar = ~
 
     Arg -> %identifier %colon Type                        : a:Dyn => raw.Arg(a.get(0).value,a.get(2))
 
-    Type  -> %identifier                                  : a:Dyn => a.get(0).value
+    Refinements -> Stmt                                   : a:Dyn => Single(a.get(0))
+                 | Stmt %comma Refinements                : a:Dyn => llist.Cons[raw.Exp](a.get(0),a.get(2))
+
+    Type  -> BaseType                                     : a:Dyn => raw.Type(a.get(0),llist.Nil[raw.Exp]())
+           | BaseType %lcurl Refinements %rcurl           : a:Dyn => raw.Type(a.get(0),a.get(2))
+
+    BaseType -> %identifier                               : a:Dyn => raw.Base(a.get(0).value) 
+              | Expression %dot %identifier               : a:Dyn => raw.Path(a.get(0),a.get(2).value)
 
     Expression -> ExprLambda                              : a:Dyn => a.get(0) 
            
@@ -65,7 +74,7 @@ val grammar: parsing.Grammar = ~
     Primary -> %identifier                                : a:Dyn => raw.Var(a.get(0).value)
              | %lparen Expression %rparen                 : a:Dyn => a.get(1)
              | %integer                                   : a:Dyn => raw.Integer(a.get(0).value)
-             | %new_ %identifier %colon %identifier %colon %block            : a:Dyn => raw.New(a.get(1).value, a.get(3).value, a.get(5).value)
+             | %new_ %identifier %colon Type %colon %block: a:Dyn => raw.New(a.get(1).value, a.get(3), a.get(5).value)
              | %lparen %rparen                            : a:Dyn => raw.UnitVal()