#14813 closed bug (fixed)

EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.2.2
Keywords: PatternMatchWarnings Cc:
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): Phab:D5094
Wiki Page:

Description

GHC warns on this program:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

import Data.Kind
import Data.Void

data SBool (z :: Bool) where
  SFalse :: SBool 'False
  STrue  :: SBool 'True

type family F (b :: Bool) (a :: Type) :: Type where
  F 'True  a = a
  F 'False _ = Void

dispatch :: forall (b :: Bool) (a :: Type). SBool b -> F b a -> a
dispatch STrue  x = x
dispatch SFalse x = case x of {}
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:22:21: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _ :: F b a
   |
22 | dispatch SFalse x = case x of {}
   |                     ^^^^

This warning is incorrect, as x is of type F 'False a, or Void, in that case alternative.

Curiously, if you ascribe either the pattern for x:

dispatch SFalse (x :: F 'False a) = case x of {}

Or the case scrutinee:

dispatch SFalse x = case x :: F 'False a of {}

Then the warning goes away.

Change History (11)

comment:1 Changed 19 months ago by RyanGlScott

The line of code which is responsible for this infelicity is here, within checkEmptyCase':

mb_candidates <- inhabitationCandidates fam_insts (idType var)

But this is checking the inhabitation candidates of the raw idType of x, which is F b a instead of Void. It seems that what needs to happen is that we need to take the local dictionary evidence in scope (i.e., liftD getDictsDs)—in this example, b ~ 'False—and somehow use that to turn F b a into F 'False a, which reduces to Void.

On the other hand, I have no idea how one would do this, as liftD getDictsDs gives you a Bag EvVar instead of, say, a substitution, it's far from clear to me how you'd "apply" a Bag EvVar...

Last edited 14 months ago by RyanGlScott (previous) (diff)

comment:2 Changed 14 months ago by RyanGlScott

Actually, I think the issue may be in an entirely different place than what I originally suspected, and the fact that it surfaces in EmptyCase may be entirely coincidental. Consider the following program, which uses an ordinary pattern-match:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

data Unit = MkUnit

data SUnit (u :: Unit) where
  SMkUnit :: SUnit 'MkUnit

type family F (u :: Unit) where
  F 'MkUnit = ()

absoluteUnit :: SUnit u -> F u -> ()
absoluteUnit SMkUnit x = case x of { () -> () }

Things get interesting when you try to put wildcard types on various spots. For example, if you put one on the scrutinee of the case expression:

absoluteUnit :: SUnit u -> F u -> ()
absoluteUnit SMkUnit x = case (x :: _) of { () -> () }

Then this is what GHC gives back:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:17:37: error:
    • Found type wildcard ‘_’ standing for ‘F 'MkUnit’
      To use the inferred type, enable PartialTypeSignatures
    • In an expression type signature: _
      In the expression: (x :: _)
      In the expression: case (x :: _) of { () -> () }
    • Relevant bindings include
        x :: F u (bound at Bug.hs:17:22)
        absoluteUnit :: SUnit u -> F u -> () (bound at Bug.hs:17:1)
   |
17 | absoluteUnit SMkUnit x = case (x :: _) of { () -> () }
   |                                     ^

Note that it says x's type is F 'MkUnit, not ()! To make things stranger, if you put an additional wildcard type on the binder for x:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

data Unit = MkUnit

data SUnit (u :: Unit) where
  SMkUnit :: SUnit 'MkUnit

type family F (u :: Unit) where
  F 'MkUnit = ()

absoluteUnit :: SUnit u -> F u -> ()
absoluteUnit SMkUnit (x :: _) = case (x :: _) of { () -> () }

Now GHC claims the type of both wildcards is ()!

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:17:28: error:
    • Found type wildcard ‘_’ standing for ‘()’
      To use the inferred type, enable PartialTypeSignatures
    • In a pattern type signature: _
      In the pattern: x :: _
      In an equation for ‘absoluteUnit’:
          absoluteUnit SMkUnit (x :: _) = case (x :: _) of { () -> () }
    • Relevant bindings include
        absoluteUnit :: SUnit u -> F u -> () (bound at Bug.hs:17:1)
   |
17 | absoluteUnit SMkUnit (x :: _) = case (x :: _) of { () -> () }
   |                            ^

Bug.hs:17:44: error:
    • Found type wildcard ‘_’ standing for ‘()’
      To use the inferred type, enable PartialTypeSignatures
    • In an expression type signature: _
      In the expression: (x :: _)
      In the expression: case (x :: _) of { () -> () }
    • Relevant bindings include
        x :: () (bound at Bug.hs:17:23)
        absoluteUnit :: SUnit u -> F u -> () (bound at Bug.hs:17:1)
   |
17 | absoluteUnit SMkUnit (x :: _) = case (x :: _) of { () -> () }
   |                                            ^

All this makes me believe that somehow, the typechecker isn't giving the correct type (or at least, an insufficiently type-family–free type) to x unless you explicitly prod GHC with redundant typing information.

Last edited 14 months ago by RyanGlScott (previous) (diff)

comment:3 Changed 14 months ago by simonpj

But () and F 'MkUnit are equal types, so it's probably a bit random which gets reported wehre. Why do you think the typechecker "isn't giving the correct type", and would would be consequences of that be?

comment:4 in reply to:  3 Changed 14 months ago by RyanGlScott

Replying to simonpj:

Why do you think the typechecker "isn't giving the correct type"

Like I said in comment:2, what I meant by "correct type" is "insufficiently type-family–free type".

and would would be consequences of that be?

The consequences are this very ticket! As explained in comment:1, F False a and Void can produce different results in the pattern-match coverage checker, so it's critical that we use the latter whenever possible.

comment:5 Changed 13 months ago by RyanGlScott

Another example of this phenomenon:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where

import Data.Void

type family F a
type instance F Int = Void

fun :: F Int -> a
fun x = case x of

Compiling this program yields no warnings, as expected. However, if you factor out the Int part like so:

fun :: i ~ Int => F i -> a

Then it will yield a warning:

$ /opt/ghc/8.4.3/bin/ghci Bug.hs
GHCi, version 8.4.3: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:12:9: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _ :: F i
   |
12 | fun x = case x of
   |         ^^^^

comment:6 Changed 13 months ago by simonpj

OK I undersatand now. My question in comment:3 was after reading comment:2. But comment:1 makes it clear why we want to improve inhabitationCandidates.

Essentially you want to normalise a type using both top-level instances and local equalities. The constraint solver does this all the time, so the Right Thing is probably just to expose a new API to the constraint solver, alongside tcCheckSatisfiability. Something like

tcNormalise :: Bag EvVar -> Type -> TcM Type

How would it work? A bit like tcCheckSatisfiability, except that after the solveGivens call solveWanteds passing a single CHoleCan constraint. It is not "solved", but it is normalised. So the solveWanteds will return a CHoleCan whose type is the desired normalised one.

For efficiency, you might want to do a quick check before invoking tcNormalise, in case the type is already an algebraic data type (a common case), in which case normalisation will be a no-op.

comment:7 Changed 13 months ago by RyanGlScott

Milestone: 8.8.1

Thanks, Simon! I'm afraid I'm not familiar enough with the solver interface in order to implement all of tcNormalise on my own, so I'm going to ask for more advice here. In particular:

  • solveSimpleGivens takes [Ct] as an arguments. How do I turn a CHoleCan into a Ct?
  • Moreover, how exactly do I build a CHoleCan? It takes a CtEvidence and a Hole as arguments. I have no idea what the Hole should be. Presumably, the CtEvidence should be a CtWanted, but that takes three other arguments in addition to ctev_pred, and I have no idea what any of them should be.
  • Also, where exactly should I be calling tcNormalise? In the pattern-match coverage checker? Somewhere else? (I wonder if it's possible to fix the buglet in the first program in comment:2 as well, which would seem to suggest we should be calling it somewhere besides the coverage checker.)

comment:8 Changed 13 months ago by simonpj

  • A CHoleCan is a Ct! (CHoleCan is a data constructor of Ct.)
  • How exactly do I build a CHoleCan? Currently they are born in one place, in TcExpr.tcUnboundId:
    tcUnboundId rn_expr unbound res_ty
     = do { ty <- newOpenFlexiTyVarTy  -- Allow Int# etc (Trac #12531)
          ; let occ = unboundVarOcc unbound
          ; name <- newSysName occ
          ; let ev = mkLocalId name ty
          ; loc <- getCtLocM HoleOrigin Nothing
          ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
                                                  , ctev_dest = EvVarDest ev
                                                  , ctev_nosh = WDeriv
                                                  , ctev_loc  = loc}
                               , cc_hole = ExprHole unbound }
    ...
    
    Perhaps you can copy that?
  • Also, where exactly should I be calling tcNormalise? Call it in pmTopNormaliseType. (It might need to become monadic to access the ambient constraints.

comment:9 Changed 13 months ago by RyanGlScott

Differential Rev(s): Phab:D5094
Status: newpatch

I barfed some code into my terminal, and by some miracle, it actually seems to work. See Phab:D5094 for the (slightly cleaned-up) barf.

comment:10 Changed 12 months ago by Krzysztof Gogolewski <krz.gogolewski@…>

In e72d788/ghc:

Normalise EmptyCase types using the constraint solver

Summary:
Certain `EmptyCase` expressions were mistakently producing
warnings since their types did not have as many type families reduced
as they could have. The most direct way to fix this is to normalise
these types initially using the constraint solver to solve for any
local equalities that may be in scope.

Test Plan: make test TEST=T14813

Reviewers: simonpj, bgamari, goldfire

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #14813

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

comment:11 Changed 12 months ago by monoidal

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.