Kim-Ee Yeoh wrote:
As for fixing the original bug, I've found that the real magic lies in the incantation (Y . unY) inserted at the appropriate places.
Aka unsafeCoerce, changing the phantom type |a|.
The type of (Y . unY) is (Y . unY) :: forall a b c. Y c a -> Y c b so modulo (Y c), it is indeed unsafeCoerce.
The need to do it is caused by wanting to erase the existential introduced by Za/MkZa.
That's not the primary reason. The earlier version of the code in my original message doesn't use existentials. We still however, need to "wobble" the type via (Y . unY) in order to typecheck.
Depending on what the phantom type is supposed to represent, this may or may not give the semantics/safety you're after.
If you're referring to the safety of the object/target language, then even without any Symantics instances, only type-correct code can compile, thanks to the finally-tagless embedding that "lifts" type-checking in the meta-language (Haskell) into type-checking for the target language. That safety isn't in the least bit compromised. The pretty-printing Symantics instance in question actually type-checks fine without unsafeCoerce or its like when written out without the additional Monad type-class abstraction and Y-Z isomorphism. Translating to the latter was entirely straightforward. Thanks to all who responded. -- View this message in context: http://www.nabble.com/Flipping-*-%3E*-%3E*-kinds%2C-or-monadic-finally-tagle... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.