[ fix ] Normalising the type of implicit box

Cf. issue idris-lang/Idris-dev#4206 for more explanations
gallais · Nov 20, 2017 · 1a0aaa5 · 1a0aaa5
1 parent d8c333d
commit 1a0aaa5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Combinators.idr b/src/Combinators.idr
@@ -19,7 +19,7 @@ lteLower mlen p = MkParser (\ plem => runParser p (lteTransitive plem mlen))
 ltLower : LT m n -> Parser toks tok mn a n -> Parser toks tok mn a m
 ltLower mltn = lteLower (lteSuccLeft mltn)
 
-implicit box : All (Parser toks tok mn a :-> Box (Parser toks tok mn a))
+implicit box : Parser toks tok mn a n -> Box (Parser toks tok mn a) n
 box = lteClose lteLower
 
 anyTok : (Inspect toks tok, Alternative mn) =>