Opened 22 months ago

Last modified 3 months ago

#12949 new bug

Pattern coverage checker ignores dictionary arguments

Reported by: dfeuer Owned by: gkaracha
Priority: normal Milestone: 8.8.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 (17)

comment:1 Changed 22 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 22 months ago by goldfire

This does indeed look like a bug to me.

comment:3 Changed 22 months ago by mpickering

Cc: gkaracha added

comment:4 Changed 22 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 22 months ago by bgamari

Milestone: 8.2.1
Owner: set to gkaracha

comment:6 in reply to:  1 Changed 21 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 21 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 21 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 21 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 21 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 19 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 19 months ago by dfeuer

Summary: Pattern coverage mistakePattern coverage checker ignores dictionary arguments

comment:13 Changed 19 months ago by simonpj

gkaracha, does that help?

Simon

comment:14 Changed 18 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

comment:15 Changed 8 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:16 Changed 6 months ago by sighingnow

Hello,

I'm working on this ticket and now I can tell what's going wrong with the case in comment:11. I think I need some help to go further and submit the patch.

Look at the example in comment:11:

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

When do checkMatches on inner case statement, we first call mkInitialUncovered to set up a NameEnv, in this function we use getTmCsDs to obtain the initial name env, we have

[(ds_d14i, foo), (ds_d14h, Nothing), (ds_d14h, foo)]

Nothing that these two foo have different Id (type), but the same Name. We then translate them as ComplexEq, only keeping the Name in PmExprVar. Then we get the initTmState.

In ConVar case of pmcheckHd, we have ComplexEq (ds_d14i, Just $pm_d14m) and use solveOneEq to decide whether it is a valid candidate PmCon. In solveOneEq, we first do deep substitution by looking up the Name of PmExprVar from env. Now ds_d14i is replaced with foo and further replaced with Nothing, then solveOneEq fails and the Just pattern is redundant.


To solve this, we need to consider both name and type of variables when do substitution. In comment:7 gkaracha proposed that

Turning Name back into Id in the checker

Should we move from PmExprVar Name to PmExprVar Id ? In varDeepLookup, when find the PmExpr from PrVarEnv, we could first check it's type then do further substitution. Do that make sense ?

comment:17 Changed 3 months ago by bgamari

Milestone: 8.6.18.8.1

These won't be fixed for 8.6, bumping to 8.8.

Note: See TracTickets for help on using tickets.