restrictCoRec is unsound

[samuel-gelineau-at-well-dot]

The following fails with Exception: matchNil: impossible

  let intOrString :: CoRec Identity '[Int, String]
      intOrString = CoRec (Identity "hello")
  case restrictCoRec intOrString of
    Left (Identity int) -> do
      print int
    Right definitelyString -> do
      case restrictCoRec (definitelyString :: CoRec Identity '[String]) of
        Left (Identity string) -> print string
        Right uninhabited -> matchNil (uninhabited :: CoRec Identity '[])

Workaround: use restrictCoRecSafe instead of restrictCoRec.

[samuel-gelineau-at-well-dot]

Let's look at the relevant definitions:

data CoRec :: (k -> *) -> [k] -> * where
  CoRec :: RElem a ts (RIndex a ts) => !(f a) -> CoRec f ts

restrictCoRec :: ... => CoRec f (t ': ts) -> Either (f t) (CoRec f ts)
restrictCoRec r = maybe (Right (unsafeCoerce r)) Left ...

I think the problem is that in the Nothing case, unsafeCoerce r does more than just reinterpreting CoRec fa :: CoRec f (t ': ts) into CoRec fa :: CoRec f ts, it also reinterprets the RElem dictionary.

Thus:

1. We start with a CoRec Identity [Int, String] containing a valid proof that String is in the second position in the list [Int, String].
2. The proof says that String is not in the first position, so the first restrictCoRec call casts this into a CoRec Identity [String] containing an invalid proof that String is in the second position in the list [String].
3. The invalid proof still says that String is not in the first position, so the second restrictCoRec call casts this into a CoRec Identity [] containing an invalid proof that String is in the second position in the list [].
4. Finally, matchNil errors out because it assumes that CoRec Identity '[] should be uninhabited, since it is not possible to construct a proof that String appears in the list []. But here, we have managed to construct a non-standard inhabitant by using unsafeCoerce to construct an invalid proof.