[GHC] #16278: Exhaustivity checking GADT with free variables
#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following example: {{{#!hs {-# language DataKinds #-} {-# language TypeFamilies #-} {-# language GADTs #-} {-# language KindSignatures #-} {-# OPTIONS_GHC -Wall -fforce-recomp #-} module GadtException where import Data.Kind (Type) import GHC.Exts data Send = Send data SocketException :: Send -> Type where LocalShutdown :: SocketException 'Send OutOfMemory :: SocketException a someSocketException :: SocketException a someSocketException = OutOfMemory foo :: Int foo = case someSocketException :: SocketException Any of LocalShutdown -> 2 OutOfMemory -> 1 }}} In `foo`, GHC's exhaustivity checker requires a pattern match on `LocalShutdown`. However, `LocalShutdown` is not an inhabitant of `SocketException Any`. What I would really like is for this to go one step further. I shouldn't even need to write the type annotation. That is, with the above code otherwise unchanged, GHC should recognize that {{{#!hs foo :: Int foo = case someSocketException of OutOfMemory -> 1 }}} handles all possible cases. Since fully polymorphic type variables become `Any` at some point during typechecking, I would expect that if this worked with the `SocketException Any` type signature, it would work without it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The pattern-match coverage checker is only able to conclude that `LocalShutdown` is an unreachable case if it can reason that `Send` and `Any` are //apart// as types (i.e., they can never possibly unify). For whatever reason, GHC appears to be unable to do this, even though `Any` is a closed type family. For most type families, this makes sense—imagine if you had: {{{#!hs type family F :: Send }}} And tried matching on a value of type `SocketException F`. GHC would be completely justified in declaring `LocalShutdown` to be a reachable case here. Even if the module you're writing didn't have any instances for `F`, due to the open-world assumption, it's possible that you might bring in another module later which declares `type instance F = 'Send`. Closed type families add an interesting wrinkle since they're, well, not open. That is, no one can write `type instance Any = 'Send`, so in theory, it should never be the case that `Any ~ 'Send`. That being said, teaching GHC to reason like this for arbitrary closed type families sounds challenging. Consider the following example: {{{#!hs data Nat = Z | S Nat type family Id (a :: k) :: k where Id x = x type family G (a :: Nat) :: k G Z = () G (S n) = Id (G n) }}} Is `G a` ever equal to `'Send`? The answer is no, but determining this requires some nontrivial reasoning. GHC would need to be able to figure out that `G a` cannot ever reduce to `'Send` by a sort of inductive argument. Moreover, GHC would also need to be aware of how `Id`, a different type family, reduces. Bottom line: while I can sympathize with your desire not to write a case for `LocalException`, actually teaching GHC the smarts to reason about this seems quite tricky. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by andrewthad): Thanks for the insights! I’m not certain that GHC replaces the polymorphic type variable with Any before the exhaustiveness check happens. (Although I suspect it does). If it does, then is unfortunate that we end up doing an apartness check for `'Send` an `Any` when what should actually happen is an apartness check for `'Send` and `forall (s :: Send). s` (talking about the second example where I omitted the type annotation). You make a good argument that teaching the compiler about apartness involving type families in the general case is difficult or maybe in possible. But there are more specific cases where deciding apartness is a more tractable problem. You could consider only non-recursive type families, only type families that don’t mention other type families, nullary type families, or the combination of all three (aka Any). From what I’ve found in the GHC wiki, it looks like the apartness check is an approximation anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => PatternMatchWarnings -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16278: Exhaustivity checking GADT with free variables -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | PatternMatchWarnings Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by andrewthad): I guess `Any` isn't really a nullary type family since the `k` argument is invisible. So, the special case that needs to be handled to make this work is "all empty type families, regardless of arity". But I think it could be done a little more broadly. Playing with the type checker, I found that this compiles: {{{#!haskell {-# language DataKinds #-} {-# language TypeFamilies #-} module TypeEqualities where type family Foo (b :: Bool) :: Bool foo :: (Foo 'True ~ 'True, Foo 'True ~ Foo 'False) => Int foo = 5 }}} My interpretation of this is that type family applications that do not reduce are not considered apart from anything. The behavior that would help me is for non-reducing type family applications with constant arguments to be considered apart from everything except for themselves. Using the above example, `Foo 'True ~ Foo 'True` would typecheck, but `Foo 'True ~ 'True` and `Foo 'True ~ Foo 'False` would both be rejected. In bulleted form, the requirement I listed are: * Non-reducing (or stuck) * Constant arguments (yes: `Foo 'True`, no: `Foo x`) I'm not sure if this is introduces inconsistencies or has any negative side effects. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16278#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC