1 files changed, 9 insertions, 8 deletions
diff --git a/lib/Parser.mly b/lib/Parser.mly
index 0390b3c..fc82d1a 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -5,13 +5,15 @@ open Ast
 %token <string> IDENT
 %token LPR RPR
 %token LBR RBR
-%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
+%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
 %token TYPE
 %token EOF
 
-%right ARROW ASTERISK
+%nonassoc DOUBLE_COLON
+%right ARROW
+%right ASTERISK
 %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM
 
 %start <Ast.expr> parse
@@ -19,24 +21,23 @@ open Ast
 %%
 
 %inline
-locate(X): e = X { Asai.Range.locate_lex $loc e }
+locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e }
 
 raw_ident: id = separated_nonempty_list(DOT, IDENT) { id }
 
 %inline
 ident: id = locate(raw_ident) { id }
 
-raw_arg: LPR; name = ident; COLON; ty = expr; RPR
-	{ { name; ty } }
-
-%inline
-arg: a = locate(raw_arg) { a }
+arg: LPR; name = ident; COLON; tp = expr; RPR
+	{ (name, tp) }
 
 raw_expr:
   | name = raw_ident
 	{ Var name }
   | LPR; e = raw_expr; RPR
 	{ e }
+  | tm = expr; DOUBLE_COLON; tp = expr
+    { Check (tm, tp) }
 
   | a = arg; ARROW; b = expr
 	{ Pi (a, b) }