Functional dependencies error message has no position information

[NeilMitchell]

When compiling the attached file (sorry its really long, it could easily be reduced to a minimal test case - although I don't think its necessary to fix the bug), I get the error message:

E:\Neil\thesis\obj\haskell2/Proof_default.hs:1:0:
    Couldn't match expected type `Expr' against inferred type `VarName'
      Expected type: ([Expr], [Expr])
      Inferred type: ([VarName], a)
    When using functional dependencies to combine
      Subst (Prop (Sat VarName)) ([VarName], a) (Prop (Sat Expr)),
        arising from a use of `/'
                     at E:\Neil\thesis\obj\haskell2/Proof_default.hs:391:17-54
      Subst (Prop (Sat Expr)) ([Expr], [Expr]) (Prop (Sat Expr)),
        arising from a use of `/'
                     at E:\Neil\thesis\obj\haskell2/Proof_default.hs:399:17-44

The error message lists two positions further down, but gives no position (or 1:0) at the top of the message. One of the positions from further down should be given - either one would do - otherwise the user may miss that there is position information available (I did at first).

[NeilMitchell]

I just got a very similar error message off slightly different code, which gives slightly different information:

E:\Neil\thesis\obj\haskell2/Proof_default.hs:1:0:
    Couldn't match expected type `VarName' against inferred type `Expr'
      Expected type: ([VarName], [Expr])
      Inferred type: ([Expr], [b])
    When using functional dependencies to combine
      Subst (Sat a) ([a], [b]) (Sat b),
        arising from the instance declaration at E:\Neil\thesis\obj\haskell2/Pr
of_default.hs:140:0
      Subst (Sat Expr) ([VarName], [Expr]) (Sat Expr),
        arising from a use of `/'
                     at E:\Neil\thesis\obj\haskell2/Proof_default.hs:402:17-43

Here the relevant position is the second one (the use, not the definition), so this bug can't just be fixed by grabbing the first position out of the list. I've again attached a sample piece of code.

[igloo]

Thanks, we'll take a look.

[igloo]

This looks like it should be easy to fix, but best to wait until the typechecker branch is merged.

[simonpj]

I've tried your example Proof_default2 with the new typechecker, and locations are better. In your second example we get

T2296b.hs:402:31:
    Couldn't match type `Expr' with `[Char]'
    In the first argument of `satE'', namely
      `(pre (body f) / (args f, xs))'
    In the first argument of `(&&)', namely
      `satE' (pre (body f) / (args f, xs))'
    In the first argument of `(==>)', namely
      `satE' (pre (body f) / (args f, xs)) && all (satE' . pre) xs'

Now, I have not unravelled all the twisty functional dependencies, but the location is at least right!

Incidentally, you have this definition earlier in the file

auto_24 = satE' $ reduce x / (vs,xs) ==> satE' $ x / (vs, xs)
 where
 x = undefined
 vs = undefined
 xs = undefined

For reasons desribed in our paper "Let should not be generalised", when fundeps and GADTs are in play we don't generalise local lets. So those x, vs, and xs are not generalised, and that gives a type error. I ignored it because it looks as if you were just stubbing out bindings.

I'll close this ticket. Do re-open it if you aren't satisfied. But I expect you've moved on to other things now!

Simon