packages feed

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 
                         ^