Locally handling an empty constraint

I need something like \case {} for constraints. See the code below. The undefined won't satisfy the type checker, nor is there anything total I found that would. The dead code warning also bubbled up out of the field incorrectly.

I think this will require new language features tangentially related to Lambdas for forall. (Both forall _. and => are invisible quantifiers.) I will link this ticket in that GHC proposal, but am making it's own issue in the first place in case this is a genuine bug that can be fixed by less intrusive means.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Asdf where

import Data.Kind
import Data.Type.Equality

data Sing a where
  X :: Sing Int
  Y :: Sing [Bool]

data Foo a = Foo a (forall b. [b] :~: a -> b)
data Bar a = Bar a (forall b. [b] ~ a => b)

f, f' :: forall a. Sing a -> Foo a

f s = Foo a b 
  where
    a :: a
    a = case s of
      X -> 0
      Y -> []
    b :: forall b. [b] :~: a -> b
    b = case s of
      X -> \case {}
      Y -> \Refl -> False

f' = \case
  X -> Foo 0  (\case {})
  Y -> Foo [] (\Refl -> False)

g, g' :: forall a. Sing a -> Bar a

g s = Bar a b 
  where
    a :: a
    a = case s of
      X -> 0
      Y -> []
    b :: forall b. [b] ~ a => b
    b = case s of
      Y -> False

g' = \case
  X -> Bar 0 undefined -- can't make this happy
  Y -> Bar [] False