#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 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 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: | -------------------------------------+------------------------------------- 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: | -------------------------------------+------------------------------------- Comment (by Krzysztof 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