Created
July 14, 2019 21:33
-
-
Save wyager/92f9cec60f6940990de630415e4d8c57 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE KindSignatures, DataKinds, GADTs, FlexibleInstances, FlexibleContexts #-} | |
main = return () | |
-- Problem: I want to (de)serialize a GADT with multiple constructors. | |
-- Any given type will only have a single valid constructor, so there should be no need to serialize a tag. | |
-- However, it is difficult to convince GHC that for all `n`, `Foo n` is deserializable. | |
-- This is presumably because the instances for `n ~ Z` and `n ~ S m` are in separate places and GHC | |
-- doesn't have logic in place to realized that that covers all possibilities. | |
-- However, I can't figure out a good way to combine the two instances so GHC is happy. | |
data Nat = Z | S Nat | |
data Foo (n :: Nat) where | |
FooZ :: Foo 'Z | |
FooN :: Int -> Foo n -> Foo ('S n) | |
-- This is a stand-in for the deserialize function of e.g. "Store" | |
class Frob a where | |
frob :: Int -> Maybe a | |
-- I tried to combine these two instances by pattern matching on singleton types, | |
-- but I ran into issues with the recursive step. | |
instance Frob (Foo 'Z) where | |
frob 0 = Just FooZ | |
frob _ = Nothing | |
instance Frob (Foo n) => Frob (Foo ('S n)) where | |
frob i = FooN i <$> frob (i-1) | |
data Blah n = Blah Int (Foo n) | |
-- GHC complains: | |
-- No instance for (Frob (Foo n)) arising from a use of ‘frob’ | |
-- But of course, we know there is an instance, for all n. | |
instance Frob (Blah n) where | |
frob i = Blah i <$> frob (i-1) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment