Opened 7 years ago

Closed 7 years ago

#7294 closed bug (fixed)

-fdefer-type-errors doesn't produce a warning

Reported by: Feuerbach Owned by:
Priority: normal Milestone: 7.6.2
Component: Compiler (Type checker) Version: 7.6.1
Keywords: Cc: roma@…, eir@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: gadt/T7293, T7294
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

With the attached code I get the expected error

sing.hs:20:8:
    Couldn't match type 'False with 'True
    Inaccessible code in
      the type signature for
        nth :: (k :< n) ~ 'True => Vec a n -> SNat k -> a

However, if I compile with -fdefer-type-errors, compilation goes clean without any errors or warnings.

Also, if I comment out the last line (with inaccessible code) and compile with -fforce-recomp -fwarn-incomplete-patterns, then I get a false warning

sing.hs:21:1: Warning:
    Pattern match(es) are non-exhaustive
    In an equation for `nth': Patterns not matched: Nil _

Attachments (1)

sing.hs (633 bytes) - added by Feuerbach 7 years ago.
test code

Download all attachments as: .zip

Change History (11)

Changed 7 years ago by Feuerbach

Attachment: sing.hs added

test code

comment:1 Changed 7 years ago by Feuerbach

In fact, the false warning is produced regardless of -fdefer-type-errors. Is it a known limitation, or should I open a separate ticket for it?

comment:2 Changed 7 years ago by Feuerbach

Component: CompilerCompiler (Type checker)

comment:3 Changed 7 years ago by goldfire

Cc: eir@… added

The second problem you mention (about the spurious warning of an incomplete pattern) is already known. See #3927.

comment:4 Changed 7 years ago by simonpj

difficulty: Unknown
Resolution: duplicate
Status: newclosed

Yes, I'm afraid #3927 is the offending ticket. Overlapping patterns are figured out *after* type checking, because it involves a sort of global analysis of the block of patterns. Fixing overlapping-pattern warnings in the presence of GADTs requires some careful thought; a nice self-contained project.

Simon

comment:5 Changed 7 years ago by simonmar

Resolution: duplicate
Status: closednew

The second problem mentioned is #3927, but the first problem is still unresolved, right?

comment:6 Changed 7 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: gadt/T7293, T7294

No, it's fine now. Without -fdefer-type-errors we get an error (test gadt/T7293); with -fdefer-type-errors we get a warning (test gadt/T7294).

Simon

comment:7 Changed 7 years ago by simonmar

Ok... was there a patch to merge, or did this get fixed as a side effect of other things?

comment:8 Changed 7 years ago by simonpj

Status: closedmerge

Harump. I'd forgotten that the branch has -fdefer-type-errors too. I think that the relevant patch is this one

commit 629d1f48b513be3cc662ea79376737dbcdb6b18f
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Oct 4 17:54:38 2012 +0100

    Improve erorr location for Given errors
    
    Note [Inaccessible code].
    Fixes Trac #7293.

 compiler/typecheck/TcErrors.lhs  |   91 +++++++++++++++++++++++---------------
 compiler/typecheck/TcRnTypes.lhs |    5 ++-
 2 files changed, 59 insertions(+), 37 deletions(-)

It may require a little adjustment to account for the fact that the branch does not have "holes". I'm not sure it's worth much effort, but perhaps worth a go.

Simon

comment:9 Changed 7 years ago by igloo

Milestone: 7.6.2

comment:10 Changed 7 years ago by igloo

Status: mergeclosed

Not worth merging, I think

Note: See TracTickets for help on using tickets.