diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr
index 1d4e245..1ecc2f3 100644
--- a/src/Core/CaseBuilder.idr
+++ b/src/Core/CaseBuilder.idr
@@ -1,8 +1,35 @@
 module Core.CaseBuilder
 
+import Core.CaseTree
 import Core.Context
 import Core.Core
 import Core.Normalise
 import Core.TT
 import Core.Value
 
+%default covering
+
+public export
+data Phase = CompileTime | RunTime
+
+data ArgType : List Name -> Type where
+     Known : RigCount -> (ty : Term vars) -> ArgType vars -- arg has type 'ty'
+     Stuck : (fty : Term vars) -> ArgType vars 
+         -- ^ arg will have argument type of 'fty' when we know enough to
+         -- calculate it
+     Unknown : ArgType vars
+         -- arg's type is not yet known due to a previously stuck argument
+
+Show (ArgType ns) where
+  show (Known c t) = "Known " ++ show c ++ " " ++ show t
+  show (Stuck t) = "Stuck " ++ show t
+  show Unknown = "Unknown"
+
+record PatInfo (pvar : Name) (vars : List Name) where
+  constructor MkInfo
+  pat : Pat
+  loc : IsVar name idx vars
+  argType : ArgType vars -- Type of the argument being inspected (i.e. 
+                         -- *not* refined by this particular pattern)
+
+
diff --git a/src/Core/CaseTree.idr b/src/Core/CaseTree.idr
index 353fff8..1a788a9 100644
--- a/src/Core/CaseTree.idr
+++ b/src/Core/CaseTree.idr
@@ -21,18 +21,15 @@ mutual
        DefaultCase : CaseTree vars -> CaseAlt vars
 
 public export
-data Pat : List Name -> Type where
-     PAs : {name : _} ->
-           FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars -> Pat vars
+data Pat : Type where
+     PAs : FC -> Name -> Pat -> Pat
      PCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
-            List (Pat vars) -> Pat vars
-     PTyCon : FC -> Name -> (arity : Nat) ->
-              List (Pat vars) -> Pat vars
-     PConst : FC -> (c : Constant) -> Pat vars
-     PArrow : FC -> (x : Name) -> Pat vars -> Pat (x :: vars) -> Pat vars
-     PLoc : {name : _} ->
-            FC -> (idx : Nat) -> IsVar name idx vars -> Pat vars
-     PUnmatchable : FC -> Term vars -> Pat vars
+            List Pat -> Pat
+     PTyCon : FC -> Name -> (arity : Nat) -> List Pat -> Pat
+     PConst : FC -> (c : Constant) -> Pat
+     PArrow : FC -> (x : Name) -> Pat -> Pat -> Pat
+     PLoc : FC -> Name -> Pat
+     PUnmatchable : FC -> Term [] -> Pat
 
 mutual
   export
@@ -54,23 +51,23 @@ mutual
     show (DefaultCase sc)
         = "_ => " ++ show sc
 
-mkPat' : List (Pat vars) -> Term vars -> Term vars -> Pat vars
-mkPat' [] orig (Local fc c idx p) = PLoc fc idx p
+mkPat' : List Pat -> Term [] -> Term [] -> Pat
+mkPat' [] orig (Ref fc Bound n) = PLoc fc n
 mkPat' args orig (Ref fc (DataCon t a) n) = PCon fc n t a args
 mkPat' args orig (Ref fc (TyCon t a) n) = PTyCon fc n a args
 mkPat' [] orig (Bind fc x (Pi _ _ s) t)
-    = PArrow fc x (mkPat' [] s s) (mkPat' [] t t)
+    = let t' = subst (Erased fc) t in
+          PArrow fc x (mkPat' [] s s) (mkPat' [] t' t')
 mkPat' args orig (App fc fn p arg) 
     = let parg = mkPat' [] arg arg in
           mkPat' (parg :: args) orig fn
-mkPat' args orig (As fc idx p ptm) 
-    = let pat = mkPat' args orig ptm in
-          PAs fc idx p pat
+mkPat' [] orig (As fc (Ref _ Bound n) ptm) 
+    = PAs fc n (mkPat' [] ptm ptm)
 mkPat' [] orig (PrimVal fc c) = PConst fc c
 mkPat' args orig tm = PUnmatchable (getLoc orig) orig
 
 export
-mkPat : Term vars -> Pat vars
+mkPat : Term [] -> Pat
 mkPat tm = mkPat' [] tm tm
 
 mutual
diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index 63bd7ec..2a56a0a 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -61,7 +61,7 @@ parameters (defs : Defs, opts : EvalOpts)
                       (\arg => eval env (arg :: locs) scope stk)
     eval env locs (App fc fn p arg) stk 
         = eval env locs fn ((p, MkClosure opts locs env arg) :: stk)
-    eval env locs (As fc idx p tm) stk = eval env locs tm stk 
+    eval env locs (As fc _ tm) stk = eval env locs tm stk 
     eval env locs (TDelayed fc r ty) stk 
         = pure (NDelayed fc r (MkClosure opts locs env ty))
     eval env locs (TDelay fc r tm) stk 
diff --git a/src/Core/TT.idr b/src/Core/TT.idr
index 5f137eb..48a36b2 100644
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@@ -297,9 +297,8 @@ data Term : List Name -> Type where
      App : FC -> (fn : Term vars) -> (p : AppInfo) -> (arg : Term vars) -> Term vars
      -- as patterns; since we check LHS patterns as terms before turning
      -- them into patterns, this helps us get it right. When normalising,
-     -- we just reduce the inner term and ignore the name
-     As : {name : _} ->
-          FC -> (idx : Nat) -> IsVar name idx vars -> Term vars -> Term vars
+     -- we just reduce the inner term and ignore the 'as' part
+     As : FC -> (as : Term vars) -> (pat : Term vars) -> Term vars
      -- Typed laziness annotations
      TDelayed : FC -> LazyReason -> Term vars -> Term vars
      TDelay : FC -> LazyReason -> Term vars -> Term vars
@@ -315,7 +314,7 @@ getLoc (Ref fc x name) = fc
 getLoc (Meta fc x y xs) = fc
 getLoc (Bind fc x b scope) = fc
 getLoc (App fc fn p arg) = fc
-getLoc (As fc idx x y) = fc
+getLoc (As fc x y) = fc
 getLoc (TDelayed fc x y) = fc
 getLoc (TDelay fc x y) = fc
 getLoc (TForce fc x) = fc
@@ -454,9 +453,7 @@ thin {outer} {inner} n (Bind fc x b scope)
     = let sc' = thin {outer = x :: outer} {inner} n scope in
           Bind fc x (assert_total (map (thin n) b)) sc'
 thin n (App fc fn p arg) = App fc (thin n fn) p (thin n arg)
-thin n (As fc idx prf tm)
-    = let (_ ** prf') = insertVar {n} _ prf in
-          As fc _ prf' (thin n tm)
+thin n (As fc nm tm) = As fc (thin n nm) (thin n tm)
 thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)
 thin n (TDelay fc r tm) = TDelay fc r (thin n tm)
 thin n (TForce fc tm) = TForce fc (thin n tm)
@@ -479,9 +476,8 @@ insertNames {outer} {inner} ns (Bind fc x b scope)
            (insertNames {outer = x :: outer} {inner} ns scope)
 insertNames ns (App fc fn p arg) 
     = App fc (insertNames ns fn) p (insertNames ns arg)
-insertNames ns (As fc idx prf tm) 
-    = let (_ ** prf') = insertVarNames {ns} idx prf in
-          As fc _ prf' (insertNames ns tm)
+insertNames ns (As fc as tm) 
+    = As fc (insertNames ns as) (insertNames ns tm)
 insertNames ns (TDelayed fc r ty) = TDelayed fc r (insertNames ns ty)
 insertNames ns (TDelay fc r tm) = TDelay fc r (insertNames ns tm)
 insertNames ns (TForce fc tm) = TForce fc (insertNames ns tm)
@@ -547,8 +543,8 @@ renameVars prf (Bind fc x b scope)
     = Bind fc x (map (renameVars prf) b) (renameVars (CompatExt prf) scope)
 renameVars prf (App fc fn p arg) 
     = App fc (renameVars prf fn) p (renameVars prf arg)
-renameVars prf (As fc idx vprf tm)
-    = As fc idx (snd (renameLocalRef prf vprf)) (renameVars prf tm)
+renameVars prf (As fc as tm)
+    = As fc  (renameVars prf as) (renameVars prf tm)
 renameVars prf (TDelayed fc r ty) = TDelayed fc r (renameVars prf ty)
 renameVars prf (TDelay fc r tm) = TDelay fc r (renameVars prf tm)
 renameVars prf (TForce fc x) = TForce fc (renameVars prf x)
@@ -620,10 +616,8 @@ mutual
      = Just (Bind fc x !(shrinkBinder b prf) !(shrinkTerm scope (KeepCons prf)))
   shrinkTerm (App fc fn p arg) prf 
      = Just (App fc !(shrinkTerm fn prf) p !(shrinkTerm arg prf))
-  shrinkTerm (As fc idx loc tm) prf 
-     = case subElem loc prf of
-            Nothing => Nothing
-            Just (_ ** loc') => Just (As fc _ loc' !(shrinkTerm tm prf))
+  shrinkTerm (As fc as tm) prf 
+     = Just (As fc !(shrinkTerm as prf) !(shrinkTerm tm prf))
   shrinkTerm (TDelayed fc x y) prf 
      = Just (TDelayed fc x !(shrinkTerm y prf))
   shrinkTerm (TDelay fc x y) prf
@@ -695,8 +689,8 @@ mkLocals {later} bs (Bind fc x b scope)
            (mkLocals {later = x :: later} bs scope)
 mkLocals bs (App fc fn p arg) 
     = App fc (mkLocals bs fn) p (mkLocals bs arg)
-mkLocals bs (As fc idx p tm) 
-    = let (_ ** p') = addVars bs p in As fc _ p' (mkLocals bs tm)
+mkLocals bs (As fc as tm) 
+    = As fc (mkLocals bs as) (mkLocals bs tm)
 mkLocals bs (TDelayed fc x y) 
     = TDelayed fc x (mkLocals bs y)
 mkLocals bs (TDelay fc x y)
@@ -711,6 +705,56 @@ export
 refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)
 refsToLocals bs y = mkLocals {later = []} bs y
 
+-- Substitute some explicit terms for names in a term, and remove those
+-- names from the scope
+namespace SubstEnv
+  data SubstEnv : List Name -> List Name -> Type where
+       Nil : SubstEnv [] vars
+       (::) : Term vars -> 
+              SubstEnv ds vars -> SubstEnv (d :: ds) vars
+
+  findDrop : {drop, idx : _} ->
+             FC -> Maybe RigCount -> IsVar name idx (drop ++ vars) -> 
+             SubstEnv drop vars -> Term vars
+  findDrop {drop = []} fc r var env = Local fc r _ var
+  findDrop {drop = x :: xs} fc r First (tm :: env) = tm
+  findDrop {drop = x :: xs} fc r (Later p) (tm :: env) 
+      = findDrop fc r p env
+
+  find : {outer, idx : _} ->
+         FC -> Maybe RigCount -> IsVar name idx (outer ++ (drop ++ vars)) ->
+         SubstEnv drop vars ->
+         Term (outer ++ vars)
+  find {outer = []} fc r var env = findDrop fc r var env
+  find {outer = x :: xs} fc r First env = Local fc r _ First
+  find {outer = x :: xs} fc r (Later p) env = weaken (find fc r p env)
+
+  substEnv : {outer : _} ->
+             SubstEnv drop vars -> Term (outer ++ (drop ++ vars)) -> 
+             Term (outer ++ vars)
+  substEnv env (Local fc r _ prf) 
+      = find fc r prf env
+  substEnv env (Ref fc x name) = Ref fc x name
+  substEnv env (Meta fc n i xs) 
+      = Meta fc n i (map (substEnv env) xs)
+  substEnv {outer} env (Bind fc x b scope) 
+      = Bind fc x (map (substEnv env) b) 
+                  (substEnv {outer = x :: outer} env scope)
+  substEnv env (App fc fn p arg) 
+      = App fc (substEnv env fn) p (substEnv env arg)
+  substEnv env (As fc as pat) 
+      = As fc (substEnv env as) (substEnv env pat)
+  substEnv env (TDelayed fc x y) = TDelayed fc x (substEnv env y)
+  substEnv env (TDelay fc x y) = TDelay fc x (substEnv env y)
+  substEnv env (TForce fc x) = TForce fc (substEnv env x)
+  substEnv env (PrimVal fc c) = PrimVal fc c
+  substEnv env (Erased fc) = Erased fc
+  substEnv env (TType fc) = TType fc
+
+export
+subst : Term vars -> Term (x :: vars) -> Term vars
+subst val tm = substEnv {outer = []} {drop = [_]} [val] tm
+
 -- Get the metavariable names in a term
 export
 getMetas : Term vars -> NameMap ()
@@ -726,7 +770,7 @@ getMetas tm = getMap empty tm
         = getMap (getMap ns (binderType b)) scope
     getMap ns (App fc fn p arg) 
         = getMap (getMap ns fn) arg
-    getMap ns (As fc idx x y) = getMap ns y
+    getMap ns (As fc as tm) = getMap ns tm
     getMap ns (TDelayed fc x y) = getMap ns y
     getMap ns (TDelay fc x y) = getMap ns y
     getMap ns (TForce fc x) = getMap ns x
@@ -750,7 +794,7 @@ getRefs tm = getMap empty tm
         = getMap (getMap ns (binderType b)) scope
     getMap ns (App fc fn p arg) 
         = getMap (getMap ns fn) arg
-    getMap ns (As fc idx x y) = getMap ns y
+    getMap ns (As fc as tm) = getMap ns tm
     getMap ns (TDelayed fc x y) = getMap ns y
     getMap ns (TDelay fc x y) = getMap ns y
     getMap ns (TForce fc x) = getMap ns x
diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr
index 8c5bae0..bbc2f54 100644
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@@ -210,10 +210,9 @@ TTC (Term vars) where
   toBuf b (App fc fn p arg) 
       = do tag 4;
            toBuf b fc; toBuf b fn; toBuf b p; toBuf b arg
-  toBuf b (As {name} fc idx p tm)
+  toBuf b (As fc as tm)
       = do tag 5;
-           toBuf b fc; toBuf b name; 
-           toBuf b idx; toBuf b tm
+           toBuf b fc; toBuf b as; toBuf b tm
   toBuf b (TDelayed fc r tm) 
       = do tag 6;
            toBuf b fc; toBuf b r; toBuf b tm
@@ -249,9 +248,9 @@ TTC (Term vars) where
              4 => do fc <- fromBuf r b; fn <- fromBuf r b
                      p <- fromBuf r b; arg <- fromBuf r b
                      pure (App fc fn p arg)
-             5 => do fc <- fromBuf r b; name <- fromBuf r b
-                     idx <- fromBuf r b; tm <- fromBuf r b
-                     pure (As {name} fc idx (mkPrf idx) tm)
+             5 => do fc <- fromBuf r b
+                     as <- fromBuf r b; tm <- fromBuf r b
+                     pure (As fc as tm)
              6 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
                      pure (TDelayed fc lr tm)
              7 => do fc <- fromBuf r b; lr <- fromBuf r b; tm <- fromBuf r b
@@ -265,9 +264,9 @@ TTC (Term vars) where
              _ => corrupt "Term"
 
 export
-TTC (Pat vars) where
-  toBuf b (PAs {name} fc idx x y) 
-      = do tag 0; toBuf b fc; toBuf b name; toBuf b idx; toBuf b y
+TTC Pat where
+  toBuf b (PAs fc x y) 
+      = do tag 0; toBuf b fc; toBuf b x; toBuf b y
   toBuf b (PCon fc x t arity xs) 
       = do tag 1; toBuf b fc; toBuf b x; toBuf b t; toBuf b arity; toBuf b xs
   toBuf b (PTyCon fc x arity xs) 
@@ -276,16 +275,16 @@ TTC (Pat vars) where
       = do tag 3; toBuf b fc; toBuf b c
   toBuf b (PArrow fc x s t)
       = do tag 4; toBuf b fc; toBuf b x; toBuf b s; toBuf b t
-  toBuf b (PLoc {name} fc idx x) 
-      = do tag 5; toBuf b fc; toBuf b name; toBuf b idx
+  toBuf b (PLoc fc x) 
+      = do tag 5; toBuf b fc; toBuf b x
   toBuf b (PUnmatchable fc x) 
       = do tag 6; toBuf b fc; toBuf b x
 
   fromBuf r b 
       = case !getTag of
-             0 => do fc <- fromBuf r b; name <- fromBuf r b;
-                     idx <- fromBuf r b; y <- fromBuf r b
-                     pure (PAs {name} fc idx (mkPrf idx) y)
+             0 => do fc <- fromBuf r b; x <- fromBuf r b;
+                     y <- fromBuf r b
+                     pure (PAs fc x y)
              1 => do fc <- fromBuf r b; x <- fromBuf r b
                      t <- fromBuf r b; arity <- fromBuf r b
                      xs <- fromBuf r b
@@ -299,9 +298,8 @@ TTC (Pat vars) where
              4 => do fc <- fromBuf r b; x <- fromBuf r b
                      s <- fromBuf r b; t <- fromBuf r b
                      pure (PArrow fc x s t)
-             5 => do fc <- fromBuf r b; name <- fromBuf r b
-                     idx <- fromBuf r b
-                     pure (PLoc {name} fc idx (mkPrf idx))
+             5 => do fc <- fromBuf r b; x <- fromBuf r b
+                     pure (PLoc fc x)
              6 => do fc <- fromBuf r b; x <- fromBuf r b
                      pure (PUnmatchable fc x)
              _ => corrupt "Pat"