Opened 10 years ago

Closed 7 years ago

#2296 closed bug (fixed)

Functional dependencies error message has no position information

Reported by: NeilMitchell Owned by: simonpj
Priority: high Milestone: 7.0.1
Component: Compiler Version: 6.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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).

Attachments (2)

Proof_default.hs (11.4 KB) - added by NeilMitchell 10 years ago.
Proof_default2.hs (11.4 KB) - added by NeilMitchell 10 years ago.

Download all attachments as: .zip

Change History (14)

Changed 10 years ago by NeilMitchell

Attachment: Proof_default.hs added

comment:1 Changed 10 years ago by 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.

Changed 10 years ago by NeilMitchell

Attachment: Proof_default2.hs added

comment:2 Changed 10 years ago by igloo

difficulty: Unknown
Milestone: 6.10 branch

Thanks, we'll take a look.

comment:3 Changed 9 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:4 Changed 9 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:5 Changed 9 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:6 Changed 8 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:7 Changed 7 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:8 Changed 7 years ago by igloo

Priority: lowhigh
Type of failure: None/Unknown

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

comment:9 Changed 7 years ago by igloo

Blocked By: 4232 added

comment:10 Changed 7 years ago by simonmar

Owner: set to simonpj

comment:11 Changed 7 years ago by simonpj

Resolution: fixed
Status: newclosed

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

comment:12 Changed 7 years ago by igloo

Blocked By: 4232 removed
Note: See TracTickets for help on using tickets.