git.iko.soy/Idris-dev
on aef8dc1 help sign in
Idris-dev/test/reg050/expected
28 lines 956 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 "~=~",
22 ambiguous use of a left-associative operator,
23 ambiguous use of a non-associative operator,
24 ambiguous use of a right-associative operator,
25 end of input, function argument,
26 matching application expression
27doubleBang mmn = do pure !!mmn
28 ^