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

Improper quantification in mutually-recursive code #1353

Closed
JoeyEremondi opened this Issue Apr 20, 2016 · 2 comments

Comments

Projects
None yet
2 participants
@JoeyEremondi
Contributor

JoeyEremondi commented Apr 20, 2016

Possibly related to #1192, but I'm not sure.

From this mailing list issue.

Someone found an example where code compiles with type annotations, but doesn't when they annotations are removed, which seems like a pretty strong violation of Elm's inference policy.

eval ac x = 
  let f = 
    (\ y -> evalRecord x) 
  in ac

evalUnit x = eval () x

evalRecord x = eval {} x

This fails when the type signature for eval is removed, with the following error:

The 1st argument to function `eval` is causing a mismatch.
3| evalUnit x = eval () x
Function `eval` is expecting the 1st argument to be:
    {}
But it is:
    ()

Here, we only wrap compileRecord in a lambda to ensure termination, which wouldn't happen with strict evaluation.

It appears that, when the signature is removed, the typechecker chooses not to give eval a polymorphic type. The uses in evalRecord and evalUnit don't instantiate it, but uses the same unification variable that was used when inferring the type for eval.

The error is not record or tuple specific, as we get a similar error with the following code:

eval ac x = let _ = evalRecord x in ac
evalUnit x = eval Nothing x
evalRecord x = eval True x

Likewise, it's not the let expression on eval causing the problem, as this also fails:

eval ac x = always ac (evalRecord x)
evalUnit x = eval Nothing x
evalRecord x = eval True x

I don't really understand the current typechecker code, because not standard Hindley Milner, but is instead doing some fancy stuff with higher-rank and higher-kind stuff.

What's worse is, according to share-elm, this bug has been present since 0.12.3, so it's not any of the new error-message reporting that's causing it.

@gregr

This comment has been minimized.

gregr commented Apr 20, 2016

Hi, original poster here. I'm not sure how Elm's inference compares with Haskell's, but I investigated with GHC and the example failed in the same way. I believe it's an issue with polymorphic recursion which is undecidable in general and would need special support.

So, maybe this is not something we should expect the compiler to be able to handle?

@JoeyEremondi

This comment has been minimized.

Contributor

JoeyEremondi commented Apr 20, 2016

Ahh, I guess you're right. I'd forgotten how the shared unification variables work for mutually-recursive functions.

I somehow had it in my head that we could typecheck eval without knowing the type of evalRecord, but that's obviously impossible.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment