Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Leaving out an argument in type declaration produces error with no line number #4578

Open
DestyNova opened this issue Oct 24, 2018 · 0 comments

Comments

@DestyNova
Copy link

I left out a List Int parameter in the declaration of rap, and the resulting error message doesn't indicate the line number (idris 1.3.0).

Steps to Reproduce

module Accumulate

rap : (Int -> Int) -> List Int -> List Int
rap f acc [] = acc
rap f acc (x :: xs) = rap f (f x :: acc) xs

Expected Behavior

An error message explaining that the type signature for rap doesn't match its declaration, along with a line number hint.

Observed Behavior

The compiler correctly notes that rap may be applied to too many arguments, but doesn't tell me the line number:

Type checking ./Accumulate.idr
 When checking left hand side of rap:
Type mismatch between
        List Int (Type of rap _ _)
and
        _ -> _ (Is rap _ _ applied to too many arguments?)

Specifically:
        Type mismatch between
                List
        and
                \uv => _ -> uv
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant