[GHC] #14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple PatternMatchWarnings | Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC warns on this program: {{{#!hs {-# 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`: {{{#!hs dispatch SFalse (x :: F 'False a) = case x of {} }}} Or the case scrutinee: {{{#!hs dispatch SFalse x = case x :: F 'False a of {} }}} Then the warning goes away. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The line of code which is responsible for this infelicity is [http://git.haskell.org/ghc.git/blob/7c173b9043f7a9a5da46c5b0cc5fc3b38d1a7019... here], within `checkEmptyCase'`: {{{#!hs 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 `F 'False a`. 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`. 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`... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs {-# 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: {{{#!hs 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`: {{{#!hs {-# 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 `()`! 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:3 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another example of this phenomenon: {{{#!hs {-# 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: {{{#!hs 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 | ^^^^ }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.8.1 Comment: 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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5094 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5094 Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5094 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Krzysztof Gogolewski <krz.gogolewski@…>): In [changeset:"e72d7880b940881d38b8c3db9a00d5d007b1458f/ghc" e72d788/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e72d7880b940881d38b8c3db9a00d5d007b1458f" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14813: EmptyCase thinks pattern match involving type family is not exhaustive, when it actually is -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.2.2 Resolution: fixed | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5094 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14813#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC