Opened 12 months ago

Last modified 8 months ago

#12949 new bug

Pattern coverage checker ignores dictionary arguments

Reported by: dfeuer Owned by: gkaracha
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.0.1
Keywords: PatternMatchWarnings Cc: gkaracha
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I disabled syntax highlighting below; the bugs highlighting single quotes made the code unreadable.

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, TypeOperators, ScopedTypeVariables, ConstraintKinds, StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall #-}

import Data.Constraint
import Data.Type.Bool

-- Bool singletons
data Boolly b where
  Falsey :: Boolly 'False
  Truey :: Boolly 'True
deriving instance Show (Boolly b)

class KnownBool b where
  knownBool :: Boolly b
instance KnownBool 'False where
  knownBool = Falsey
instance KnownBool 'True where
  knownBool = Truey

-- OrRel a b r expresses all the usual implications inherent
-- in the statement that r ~ (a || b).
type OrRel (a :: Bool) (b :: Bool) (r :: Bool) :: Constraint =
  (r ~ (a || b),
   If r
      (If (Not a) (b ~ 'True) (() :: Constraint),
       If (Not b) (a ~ 'True) (() :: Constraint))
      (a ~ 'False, b ~ 'False))

-- Given known Bools, their disjunction is also known

abr :: forall a b r p1 p2 . (OrRel a b r, KnownBool a, KnownBool b) => p1 a -> p2 b -> Dict (KnownBool r)
abr _ _ = case knownBool :: Boolly a of
            Truey -> Dict
            Falsey -> case knownBool :: Boolly b of
              Truey -> Dict -- Problematic match
              Falsey -> Dict

The trouble is that GHC warns that the problematic match is redundant, which it is not. If I remove it, GHC fails to warn that the patterns are incomplete, which they are.

Change History (14)

comment:1 Changed 12 months ago by dfeuer

Note that everything works as expected if I pass in the Boolly values explicitly. Perhaps the pattern coverage checker is confusing knownBool called at different types?

comment:2 Changed 12 months ago by goldfire

This does indeed look like a bug to me.

comment:3 Changed 12 months ago by mpickering

Cc: gkaracha added

comment:4 Changed 12 months ago by gkaracha

Keywords: PatternMatchWarnings added

Ah, yes, I think so too. First #11984 freshened variables too much (I still haven't managed to fix it), now this freshens them too little. I will take a look at this one too.

comment:5 Changed 11 months ago by bgamari

Milestone: 8.2.1
Owner: set to gkaracha

comment:6 in reply to:  1 Changed 11 months ago by gkaracha

Replying to dfeuer:

Note that everything works as expected if I pass in the Boolly values explicitly. Perhaps the pattern coverage checker is confusing knownBool called at different types?

Indeed you are right, this is not a bug in the type constraints that the checker generates but the term constraints. I expected the knownBools to be already desugared to (knownBool $dKnownBool_a) and (knownBool $dKnownBool_b) since they are overloaded but I was mistaken. Hence, it now (wrongly) generates {knownBool ~ Falsey, knownBool ~ Truey} which is of course unsatisfiable.

comment:7 Changed 11 months ago by gkaracha

I guess I could fix this by

  • Turning Name back into Id in the checker (incl. the term oracle)
  • Checking equality on term variables taking their type into account, something like this:
        tmEqVar :: Id -> Id -> Bool
        tmEqVar x1 x2 = (idName x1 == idName x2) && (idType x1 `eqType` idType x2)
    

Does that make sense?

PS. I am not happy to have types in the term oracle (it's not as modular as I liked it to be) but I don't know of any other way to "restore" the implicit invariant that each variable has only one type.

comment:8 Changed 11 months ago by dfeuer

I believe the instance selection is all done in the type checker. Hopefully someone can tell you how to get that info!

comment:9 Changed 11 months ago by simonpj

Indeed you are right, this is not a bug in the type constraints that the checker generates but the term constraints. I expected the knownBools to be already desugared to (knownBool $dKnownBool_a) and (knownBool $dKnownBool_b) since they are overloaded but I was mistaken.

I'm going to need more guidance before I can help. Can you give instructions to reproduce the bit you think is unexpected?

I compiled the program (adding a definition for Dict which you omitted), with -ddump-ds and got

...
        ds_d3Xn = knownBool @ a $dKnownBool_a3Ux } in
...
            ds_d3Xo = knownBool @ b $dKnownBool_a3UL } in

which is what you expect. This is post-desugaring. Before desugaring there'll be a HsWrapper involved.

Anyway, please show me specifically what you think it unexpected.


Incidentally, the constraint signatures don't seem to work. Compiling

type T a = Eq a :: Constraint

yields a syntax error, as does

type T a :: Constraint = Eq a

I must be doing something stupid. But what?

comment:10 in reply to:  9 Changed 11 months ago by gkaracha

Replying to simonpj:

Indeed you are right, this is not a bug in the type constraints that the checker generates but the term constraints. I expected the knownBools to be already desugared to (knownBool $dKnownBool_a) and (knownBool $dKnownBool_b) since they are overloaded but I was mistaken.

I'm going to need more guidance before I can help. Can you give instructions to reproduce the bit you think is unexpected?

I compiled the program (adding a definition for Dict which you omitted), with -ddump-ds and got

...
        ds_d3Xn = knownBool @ a $dKnownBool_a3Ux } in
...
            ds_d3Xo = knownBool @ b $dKnownBool_a3UL } in

which is what you expect. This is post-desugaring. Before desugaring there'll be a HsWrapper involved.

Ah, great, thanks! This may be sufficient: I think that translatePat in deSugar/Check.hs just needs to look at the wrapper in the CoPat case then. It already inspects it for dropping trivial coercions, as an optimization. I'll look into it and ping you if anything else gets in the way (I hope not).

comment:11 Changed 9 months ago by dfeuer

In case it's helpful, I've come up with a much simpler case:

{-# LANGUAGE ScopedTypeVariables #-}
module Exh where

class Foo a where
  foo :: Maybe a

data Result a b = Neither | This a | That b | Both a b

q :: forall a b . (Foo a, Foo b) => Result a b
q = case foo :: Maybe a of
      Nothing -> case foo :: Maybe b of
                   Nothing -> Neither
                   Just c -> That c
      Just i -> case foo :: Maybe b of
                   Nothing -> This i
                   Just c -> Both i c

This produces the following warnings, both of them incorrect:

Exh.hs:13:20: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In a case alternative: Just c -> ...
   |
13 |                    Just c -> That c
   |                    ^^^^^^^^^^^^^^^^

Exh.hs:15:20: warning: [-Woverlapping-patterns]
    Pattern match is redundant
    In a case alternative: Nothing -> ...
   |
15 |                    Nothing -> This i
   |                    ^^^^^^^^^^^^^^^^^

comment:12 Changed 9 months ago by dfeuer

Summary: Pattern coverage mistakePattern coverage checker ignores dictionary arguments

comment:13 Changed 9 months ago by simonpj

gkaracha, does that help?

Simon

comment:14 Changed 8 months ago by bgamari

Milestone: 8.2.18.4.1

Given that 8.2.1-rc1 is imminent, I'm bumping these off to the 8.4

Note: See TracTickets for help on using tickets.