Binder-swap for singletons looks fishy
Reading #21229 (closed) and Note [Care with binder-swap on dictionaries]
, I wondered if there might not be a similar issue with singletons such as SNat
as there is with dictionaries. Perhaps this is related to #23109?
Imagine we had this:
f :: forall (a :: Natural) . SNat a -> blah
h = \ @(a :: Natural) (snat :: SNat a)
let co = SNat[0] <a> :: SNat a ~R# Natural
case snat |> co of wild
0 -> f @0 (0 |> sym (SNat[0] <0>))
1 -> f @a snat
Now we can binder-swap (snat
is not a dictionary Id) and unfold wild
to get
h = \ @(a :: Natural) (snat :: SNat a)
let co = SNat[0] <a> :: SNat a ~R# Natural
case snat |> co of wild
0 -> f @0 (0 |> sym (SNat[0] <0>))
1 -> f @a (1 |> sym co)
Unlike the example from the Note, we do not directly specialise f @a d
to f @a (1 |> sym co)
because the argument is not a dictionary. But f @a (1 |> sym co)
still seems problematic, because it is valid only within the body of the case (outside of the case we have no reason to believe that the a = 1
), but there is nothing to stop it floating.
Here's a more concrete example:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module SNatBinderSwap where
import Data.Kind (Type)
import Data.Type.Equality
import GHC.TypeNats
type G :: Nat -> Type -> Type -> Type
type family G n s t where
G 0 s _ = s
G _ _ t = t
newtype N n s t = MkN { unN :: G n s t }
{-# NOINLINE f #-}
f :: SNat a -> N a Bool Char
f x | Just Refl <- testEquality x (SNat @0) = MkN True
| Just Refl <- testEquality x (SNat @1) = MkN 'x'
h :: SNat a -> N a Bool Char
h snat
| Just Refl <- testEquality snat (SNat @1) = f snat
| Just Refl <- testEquality snat (SNat @0) = f snat
Compiling this with 9.6.1 gives:
h2 :: Natural
h2 = NS 0##
h1 :: forall {a :: Nat}. N a Bool Char
h1
= \ (@(a_aHj :: Nat)) ->
f @a_aHj (h2 `cast` <Co:3> :: Natural ~R# SNat a_aHj)
h :: forall (a :: Nat). SNat a -> N a Bool Char
h = \ (@(a_aHj :: Nat)) (snat_X1 :: SNat a_aHj) ->
case snat_X1 `cast` <Co:2> :: SNat a_aHj ~R# Natural of wild_aJ1 {
NS x1_aJ2 ->
case x1_aJ2 of {
__DEFAULT -> case h3 of wild2_00 { };
0## -> h1 @a_aHj;
1## -> f @a_aHj (wild_aJ1 `cast` <Co:3> :: Natural ~R# SNat a_aHj)
};
NB x1_aJa -> case h3 of wild1_00 { }
}
Now h1
looks fishy. It claims to have type N a Bool Char
, but its implementation passes 0 as the evidence for SNat a
. Hence it will always evaluate to MkN True
, and if we were to somehow arrange to call h1
at some non-zero Nat
, we would have a type soundness bug.
I haven't yet managed to construct an example that actually exploits this. But is there some principled reason why it is safe, or are we just relying on being lucky?
Perhaps the underlying issue here is that SNat
is not a "real" singleton type, so we don't have a way to pattern-match on it and keep track of the evidence that we have done so.