Open samuel-gelineau-at-well-dot opened 10 months ago
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:
CoRec Identity [Int, String]
containing a valid proof that String
is in the second position in the list [Int, String]
.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]
.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 []
.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.
The following fails with
Exception: matchNil: impossible
Workaround: use
restrictCoRecSafe
instead ofrestrictCoRec
.