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