Hello, My guess is that the Nat parameter in SNat gets erased, and both types end up with the same runtime representation. I'm not sure how reliable this is. Have you tried using a SNatClass that works more like KnownNat, that is, having a method that returns a Nat? Best regards, Marcin Mrotek