git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/reg050/expected
27 lines 945 B history raw
1badbangop.idr:16:1:When elaborating right hand side of opUse:
2When elaborating an application of function Prelude.Monad.>>=:
3 Can't unify
4 List Integer
5 with
6 argTy -> retTy
7
8 Specifically:
9 Can't unify
10 List
11 with
12 \{uv0} => argTy -> uv
13./baddoublebang.idr:6:26: error: not
14 a terminator, expected: "$",
15 "$>", "&&", "*", "+", "++", "-",
16 "->", ".", "/", "/=", "::", ";",
17 "<", "<$", "<$>", "<*>", "<+>",
18 "<->", "<<", "<=", "<|>", "=",
19 "==", ">", ">=", ">>", ">>=",
20 "\\\\", "`", "in", "||", "~=~",
21 ambiguous use of a left-associative operator,
22 ambiguous use of a non-associative operator,
23 ambiguous use of a right-associative operator,
24 end of input, function argument,
25 matching application expression
26doubleBang mmn = do pure !!mmn
27 ^