Opened 5 weeks ago

Last modified 4 weeks ago

#14253 new bug

Pattern match checker mistakenly concludes pattern match on pattern synonym is unreachable

Reported by: bgamari Owned by:
Priority: high Milestone: 8.4.1
Component: Compiler Version: 8.2.1
Keywords: PatternSynonyms, PatternMatchWarnings Cc: George, gkaracha, dfeuer, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #11984, #14098 Differential Rev(s): Phab:D4005
Wiki Page:

Description

Consider this program,

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}

module Test where

import GHC.Exts
import Data.Kind

data TypeRep (a :: k) where
    Con :: TypeRep (a :: k)
    TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
               TypeRep a
            -> TypeRep b
            -> TypeRep (a -> b)

pattern Fun :: forall k (fun :: k). ()
            => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (arg :: TYPE r1) (res :: TYPE r2).
               (k ~ Type, fun ~~ (arg -> res))
            => TypeRep arg
            -> TypeRep res
            -> TypeRep fun
pattern Fun arg res <- TrFun arg res
  where Fun arg res = undefined

data Dynamic where
    Dynamic :: forall a. TypeRep a -> a -> Dynamic

-- Removing this allows compilation to proceed
{-# COMPLETE Con #-}

dynApply :: Dynamic -> Dynamic -> Maybe Dynamic
-- Changing Fun to TrFun allows compilation to proceed
dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
dynApply _ _ = Nothing

As written the program fails with,

test.hs:34:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘dynApply’:
        dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = ...
   |
34 | dynApply (Dynamic (Fun ta tr) f) (Dynamic ta' x) = undefined
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This can be worked around by doing one of the following,

  1. Removing the COMPLETE pragma
  2. Changing the use of the Fun pattern synonym into a use of the TrFun constructor.

Something is quite wrong here.

Change History (14)

comment:1 Changed 5 weeks ago by dfeuer

Cc: gkaracha dfeuer added

comment:2 Changed 5 weeks ago by RyanGlScott

Cc: RyanGlScott added
Keywords: PatternSynonyms PatternMatchWarnings added

Here is a much simpler way to trigger the issue:

{-# LANGUAGE PatternSynonyms #-}
module Test where

data T = MkT1 | MkT2
pattern MkT2' = MkT2
{-# COMPLETE MkT1 #-}

newtype S = MkS T

u :: S -> Bool
u (MkS MkT2') = True
u _           = False
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Test             ( Test.hs, interpreted )

Test.hs:11:1: warning: [-Woverlapping-patterns]
    Pattern match has inaccessible right hand side
    In an equation for ‘u’: u (MkS MkT2') = ...
   |
11 | u (MkS MkT2') = True
   | ^^^^^^^^^^^^^^^^^^^^

The fact that MkT2' occurs inside of another constructor MkS seems to be important, since changing u to be of type T -> Bool and matching directly on MkT2' in the first case resolves the issue.

Last edited 5 weeks ago by RyanGlScott (previous) (diff)

comment:3 Changed 5 weeks ago by simonpj

I'm puzzled though. The {-# COMPLETE MkT1 #-} pragma seems like a manifest lie. It claims that any matching on MkT2 is inaccessible doesn't it?

comment:4 in reply to:  3 Changed 5 weeks ago by dfeuer

Replying to simonpj:

I'm puzzled though. The {-# COMPLETE MkT1 #-} pragma seems like a manifest lie. It claims that any matching on MkT2 is inaccessible doesn't it?

COMPLETE pragmas are allowed to be lies. Perhaps values built from MkT1 are never visible outside this module.

comment:5 Changed 5 weeks ago by simonpj

OK, but then lies might give rise to error messages or warnings that lie, mightn't they. As here.

We need a specification of the expected behaviour of lying COMPLETE pragmas before we can discuss what programs like these "should" do. Or we could say "if the pragma lies, the compiler can do what it likes".

comment:6 Changed 5 weeks ago by dfeuer

Ah, I think Ryan's simplification goes a bit too far, perhaps. I think you'll find Ben's original version convincing.

comment:7 Changed 5 weeks ago by RyanGlScott

I'm not sure why the original program would be any more honest, since it claims that matching on TrFun is inaccessible, right? That is, Con is to MkT1 as TrFun is to MkT2 as Fun is to MkT2' as Dynamic is to S as dynApply is to u. Or am I missing something?

comment:8 in reply to:  7 Changed 5 weeks ago by dfeuer

Replying to RyanGlScott:

I'm not sure why the original program would be any more honest, since it claims that matching on TrFun is inaccessible, right? That is, Con is to MkT1 as TrFun is to MkT2 as Fun is to MkT2' as Dynamic is to S as dynApply is to u. Or am I missing something?

Ah, simply because I didn't read it correctly. Ben came to this dishonest reduction from a perfectly honest example!

comment:9 Changed 5 weeks ago by RyanGlScott

Regardless of the example's moral integrity, I posit that it exhibits buggy behavior.

First, let's try to hammer out what should happen here. There's something of a specification buried in the annals of the GHC wiki here. (Why is this not in the users' guide?) The relevant bit is:

When the pattern match checker requests a set of constructors for a type constructor T, we now return a list of sets which include the normal data constructor set and also any COMPLETE pragmas of type T. We then try each of these sets, not warning if any of them are a perfect match. In the case the match isn't perfect, we select one of the branches of the search depending on how good the result is.

The results are prioritised in this order.

  1. Fewest uncovered clauses
  2. Fewest redundant clauses
  3. Fewest inaccessible clauses
  4. Whether the match comes from a COMPLETE pragma or the built-in set of data constructors for a type constructor.

In the example above, we're matching on something of type T, so we have the built-in constructor set {MkT1, MkT2} as well as the COMPLETE set {MkT1}. Since u only matches on MkT2', the latter set {MkT1} (the COMPLETE set) has the fewest number of uncovered clauses, so we use that for reporting warnings. Therefore, the error that we would expect to get (but don't, due to this bug) is:

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: MkS MkT1

Does that sound agreeable?

Last edited 5 weeks ago by RyanGlScott (previous) (diff)

comment:10 Changed 5 weeks ago by simonpj

Does that sound agreeable?

OK with me.

  • Do add those rules to the documentation of COMPLETE in the user guide

comment:11 Changed 5 weeks ago by RyanGlScott

Phab:D4005 adds the rules to the GHC users' guide (proofreaders wanted).

As for why this bug happens in the first place, I have a strong hunch that there's a symptom in common with #11984 (and #14098). The reason is because while this give a warning:

u :: S -> Bool
u (MkS MkT2') = True
    Pattern match has inaccessible right hand side
    In an equation for ‘u’: u (MkS MkT2') = ...

You can work around the issue using the same trick in https://ghc.haskell.org/trac/ghc/ticket/11984#comment:7 :

u :: S -> Bool
u (MkS x) = case x of
              MkT2' -> True

After this, instead of emitting the garbage inaccessible right-hand-side warning from before, GHC will warn:

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: MkT1

As we would expect. So now we need to figure out why there is a discrepancy between the pattern match checker's coverage of case and nested constructors. (I'm hoping I gain some insight after talking to SPJ about this part of the codebase tomorrow.)

comment:12 Changed 5 weeks ago by Ben Gamari <ben@…>

In acd346e3/ghc:

testsuite: Add testcase for #14253

Reviewers: austin

Subscribers: rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3997

comment:13 Changed 4 weeks ago by Ryan Scott <ryan.gl.scott@…>

In 0e60cc1/ghc:

Document how GHC disambiguates between multiple COMPLETE sets

Summary:
Up until now, the knowledge of how GHC chooses which
`COMPLETE` set to use in the presence of multiple applicable
`COMPLETE` sets for a single data type constructor was only
documented in the GHC wiki. But this really should be advertised to
anyone who uses `COMPLETE` pragmas heavily, so per SPJ's advice in
https://ghc.haskell.org/trac/ghc/ticket/14253#comment:10, this adds
this wisdom to the GHC users' guide.

Test Plan: Read it

Reviewers: austin, bgamari

Subscribers: mpickering, rwbarton, thomie

GHC Trac Issues: #14253

Differential Revision: https://phabricator.haskell.org/D4005

comment:14 Changed 4 weeks ago by dfeuer

Differential Rev(s): Phab:D4005
Note: See TracTickets for help on using tickets.