idris-0.9.16: test/reg050/expected
badbangop.idr:16:1:When elaborating right hand side of opUse:
When elaborating an application of function Prelude.Monad.>>=:
Can't unify
List Integer
with
argTy -> retTy
Specifically:
Can't unify
List
with
\{uv0} => argTy -> uv
./baddoublebang.idr:6:26: error: not
a terminator, expected: "$",
"$>", "&&", "*", "+", "++", "-",
"->", ".", "/", "/=", "::", ";",
"<", "<#>", "<$", "<$>", "<*>",
"<+>", "<->", "<<", "<=", "<|>",
"=", "==", ">", ">=", ">>",
">>=", "\\\\", "`", "in", "||",
"~=~",
ambiguous use of a left-associative operator,
ambiguous use of a non-associative operator,
ambiguous use of a right-associative operator,
end of input, function argument,
matching application expression
doubleBang mmn = do pure !!mmn
^