Opened 8 months ago

Last modified 7 months ago

#16278 new bug

Exhaustivity checking GADT with free variables

Reported by: andrewthad Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.3
Keywords: PatternMatchWarnings Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (4)

comment:1 Changed 8 months ago 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:

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.

comment:2 Changed 8 months ago 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.

comment:3 Changed 7 months ago by simonpj

Keywords: PatternMatchWarnings added

comment:4 Changed 7 months ago 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:

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

Note: See TracTickets for help on using tickets.