Drop the Helper and IsEq stuff. You need incoherent instances for this, I think, because there are two valid permutations for '[b, a] '[a, b] if a and b are instantiated as the same type. Type families won’t cut it because the apartness check balks at that possibility.
Replacing your CInsert instances with the below should do it.
instance (xs ~ ys) => CInsert x xs (x : ys) where
cinsert = IN
instance {-# INCOHERENT #-} CInsert x xs ys => CInsert x (y : xs) (y : ys) where
cinsert = IS cinsert