Fix VHPi and VPi checking

Sometimes you need to compare VHPi and VPi directly like in the
following case:

```
let x = < Foo : Natural >.Foo
in let y = \(Foo : Natural) -> < Foo : Natural >.Foo Foo
in let list = [x, y]
in list
```

Signed-off-by: Alex Humphreys <alex.humphreys@here.com>

Idrall/Check.idr

@@ -452,7 +452,7 @@ mutual
   readBackTyped ctx (VConst _) (VUnion a) = do
     a' <- traverse (readBackUnion ctx) (toList a)
     Right (EUnion (fromList a'))
-  readBackTyped ctx (VUnion _) (VInject a k arg) = -- TODO refactor nested cases
+  readBackTyped ctx (VUnion _) (VInject a k arg) =
     let kV = lookup k a in
     case (kV, arg) of
          (Just (Just k'), Just arg') =>
@@ -479,10 +479,6 @@ mutual
 unexpected : Ctx -> String -> Value -> Either Error a
 unexpected ctx str v = Left (Unexpected str v)
 
-isPi : Ctx -> Value -> Either Error (Ty, Closure)
-isPi _ (VPi a b) = Right (a, b)
-isPi ctx other = unexpected ctx "Not a Pi type" other
-
 isInteger : Ctx -> Value -> Either Error ()
 isInteger _ VInteger = Right ()
 isInteger ctx other = unexpected ctx "Not Integer" other
@@ -574,11 +570,13 @@ mutual
   check ctx (EConst CType) (VConst Kind) = Right ()
   check ctx (EConst Kind) (VConst Sort) = Right ()
   check ctx (EConst Sort) (VConst Sort) = Left SortError -- TODO check what happens here
-  check ctx (ELam x ty body) t
-    = do (a,b) <- isPi ctx t
-         -- check ctx ty a TODO use ty?
+  check ctx (ELam x ty body) (VPi a b)
+    = do -- TODO use ty?
          xV <- evalClosure b (VNeutral a (NVar x))
          check (extendCtx ctx x a) body xV
+  check ctx (ELam x ty body) (VHPi i ty' f) = do
+    check (extendCtx ctx x ty') body (f ty')
+  check ctx (ELam x ty body) other = unexpected ctx "Not a Pi type" other
   check ctx (EEquivalent x y) (VConst CType) = do
     xV <- eval (mkEnv ctx) x
     yV <- eval (mkEnv ctx) y
@@ -627,10 +625,16 @@ mutual
          Right (VPi xTy (MkClosure (mkEnv ctx) x tyRb bRb))
   synth ctx (EApp rator rand)
     = do funTy <- synth ctx rator
-         (a, b) <- isPi ctx funTy
-         check ctx rand a
-         rand' <- eval (mkEnv ctx) rand
-         evalClosure b rand'
+         case funTy of
+              (VPi a b) => do
+                 check ctx rand a
+                 rand' <- eval (mkEnv ctx) rand
+                 evalClosure b rand'
+              (VHPi i b f) => do
+                 check ctx rand b
+                 rand' <- eval (mkEnv ctx) rand
+                 Right (f rand')
+              other => unexpected ctx "Not a Pi type" other
   synth ctx (ELet x ann v e)
     = case ann of
            Nothing =>

Idrall/Parser.idr

@@ -131,11 +131,11 @@ field = do
   pure (\e => (EField e i))
 
 table : OperatorTable (Expr ImportStatement)
-table = [ [ Infix appl AssocLeft]
+table = [ [ Postfix field]
+        , [ Infix appl AssocLeft]
         , [ Infix (do (token "->" <|> token "→") ; pure (EPi "_")) AssocLeft ]
         , [ Infix (do token ":"; pure EAnnot) AssocLeft]
         , [ Infix (do (token "===" <|> token "≡"); pure EEquivalent) AssocLeft]
-        , [ Postfix field]
         , [ Prefix (do token "assert"; token ":"; pure EAssert)]
         , [ Infix (do token "&&"; pure EBoolAnd) AssocLeft]
         , [ Infix (do token "#"; pure EListAppend) AssocLeft]]