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