Exhaustivity checking GADT with free variables

Consider the following example:

{-# 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

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.

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

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:

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:

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.

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.

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:

{-# 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.

added Pnormal label

added GADTs TypeFamilies pattern match warnings labels

Andres Löh provides another example of GHC's inability to reason about closed type families in pattern-match coverage checking (adapted from https://github.com/well-typed/gp-zurihac-2020/blob/d7755f8842c073575d88fc26895c7ea8ca1c2114/Section_2_4.hs):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Section_2_4 where

import Data.Kind
import Data.Proxy
import GHC.TypeLits

data Representation =
    Sum Representation Representation
  | Constructor Symbol Representation
  | Product Representation Representation
  | Unit
  | Atom Type

type family Interpret (r :: Representation) :: Type where
  Interpret (Sum r s) = Either (Interpret r) (Interpret s)
  Interpret (Constructor n r) = Interpret r
  Interpret (Product r s) = (Interpret r, Interpret s)
  Interpret Unit = ()
  Interpret (Atom a) = a

data SRepresentation (c :: Type -> Constraint) (r :: Representation) where
  SSum :: SRepresentation c r -> SRepresentation c s -> SRepresentation c (Sum r s)
  SConstructor :: KnownSymbol n => Proxy n -> SRepresentation c r -> SRepresentation c (Constructor n r)
  SProduct :: SRepresentation c r -> SRepresentation c s -> SRepresentation c (Product r s)
  SUnit :: SRepresentation c Unit
  SAtom :: c a => SRepresentation c (Atom a)

class Top a
instance Top a

genum :: IsEnumRepresentation r => SRepresentation Top r -> [Interpret r]
genum (SSum r s) = (Left <$> genum r) ++ (Right <$> genum s)
genum (SConstructor _ _) = [()]

type family IsEnumRepresentation (r :: Representation) :: Constraint where
  IsEnumRepresentation (Sum r s) = (IsEnumRepresentation r, IsEnumRepresentation s)
  IsEnumRepresentation (Constructor n r) = r ~ Unit

If you compile this with -Wincomplete-patterns, GHC will complain thusly:

$ /opt/ghc/8.10.1/bin/ghc Section_2_4.hs -Wincomplete-patterns -fforce-recomp
[1 of 1] Compiling Section_2_4      ( Section_2_4.hs, Section_2_4.o )

Section_2_4.hs:37:1: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In an equation for ‘genum’:
        Patterns not matched:
            SProduct _ _
            SUnit
            SAtom
   |
37 | genum (SSum r s) = (Left <$> genum r) ++ (Right <$> genum s)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

But these three cases are impossible due to the IsEnumRepresentation r constraint, which will reject the type indices of those three constructors. For example, if you try to invoking genum SAtom, it will be rejected with a Could not deduce: IsEnumRepresentation ('Atom ()) error.

Part of the problem is that closed type families are used by plugins to implement arbitrary behavior. If GHC reasoned about apartness for closed type families, we would need to give plugin authors another hook to this behavior. #9840 (closed) may be a nice read for further thoughts on that point.

Very true. I don't suppose the GHC distinguishes "truly" empty closed type families from closed type families augmented with special plugin-defined equational rules?

No -- it doesn't know the difference. This is why I advocate in #9840 (comment 98795) that we organize our menagerie of type formers so that we can identify what's missing and whether the missing bits might be useful.

mentioned in issue #13248