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

Typo in return type of a function gives misleading error message #4559

Open
xoltar opened this issue Sep 14, 2018 · 0 comments
Open

Typo in return type of a function gives misleading error message #4559

xoltar opened this issue Sep 14, 2018 · 0 comments

Comments

@xoltar
Copy link
Contributor

xoltar commented Sep 14, 2018

If you write the wrong thing for a return type (e.g. bool instead of Bool), the error message is phrased in terms of 'iType', a word the user never wrote.

Steps to Reproduce

error : a -> bool
error _ = True

Expected Behavior

Idris> :l error
Type checking ./error.idr
error.idr:3:11-14:
|
3 | error _ = True
| ~~~~
When checking right hand side of error with expected type
bool (return type of error.error)

Type mismatch between
Bool (Type of True)
and
bool (Expected type)

error.idr.txt

Holes: Main.error

Observed Behavior

Idris> :l error
Type checking ./error.idr
error.idr:3:11-14:
|
3 | error _ = True
| ~~~~
When checking right hand side of error with expected type
iType

Type mismatch between
Bool (Type of True)
and
iType (Expected type)

Holes: Main.error

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