Ticket #366 (closed feature request: fixed)

Opened 8 years ago

Last modified 4 years ago

incomplete patterns and GADT

Reported by: nobody Owned by:
Priority: normal Milestone: _|_
Component: Compiler Version: None
Keywords: Cc: jcpetruzza@…, drl@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: tc215, deSugar/should_compile/GadtOverlap Blocked By:
Blocking: Related Tickets:

Description (last modified by igloo) (diff)

I would like to compile with 
-fwarn-incomplete-patterns and use GADTs, 
but I have bogus error messages. 
Suppose I define : 
 
data T a where 
    C1 :: T Char 
    C2 :: T Float 
 
then a function : 
 
exhaustive :: T Char -> Char 
exhaustive C1 = ' ' 
 
If I compile with incomplete pattern warnings, 
I get that my function "exhaustive" is not 
exhaustive. 
But if I add a case : 
 
exhaust C2 = ' ' 
 
then the compiler accurately warns me that this 
case is inaccessible. 
Would it be possible to add the accessibility check 
when compiling with incomplete patterns detection ? 

Change History

Changed 7 years ago by igloo

  • description modified (diff)
  • testcase set to tc215
  • difficulty set to Unknown
  • architecture set to Unknown
  • milestone set to 6.8
  • os set to Unknown

Changed 7 years ago by igloo

There's another case in 462.

Changed 6 years ago by guest

  • cc jcpetruzza@… added

Changed 6 years ago by simonpj

  • cc drl@… added
  • milestone changed from 6.8 branch to 6.10 branch

Dan Licata is planning to work on this.

Simon

Changed 5 years ago by simonmar

  • component changed from None to Compiler
  • milestone changed from 6.10 branch to _|_

Could be done with #595.

Changed 5 years ago by simonmar

  • architecture changed from Unknown to Unknown/Multiple

Changed 5 years ago by simonmar

  • os changed from Unknown to Unknown/Multiple

Changed 4 years ago by igloo

  • owner nobody deleted
  • status changed from assigned to new

Changed 4 years ago by simonpj

  • status changed from new to closed
  • testcase changed from tc215 to tc215, deSugar/should_compile/GadtOverlap
  • resolution changed from None to fixed

I have not done the full overhaul envisaged by #595, but it turned out to be rather easy to make GADTs play nicely with overlapping-pattern warnings.

   * Take account of GADTs when reporting patterm-match overlap
   Ignore-this: 7dcbdcb91021e83e6e6208a2e68c50c9
   When matching against a GADT, some of the constructors may be impossible.
    For example
   	data T a where
             T1 :: T Int
             T2 :: T Bool
             T3 :: T a
        f :: T Int ->  Int
        f T1 = 3
        f T3 = 4

   Here, does not have any missing cases, despite omittting T2, because
   T2 :: T Bool.

   This patch teaches the overlap checker about GADTs, which happily
   turned out to be rather easy even though the overlap checker needs
   a serious rewrite.

Simon

Note: See TracTickets for help on using tickets.