Skip to content

Instantly share code, notes, and snippets.

@guibou
Last active August 10, 2022 17:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save guibou/84333621ff0e6f9374b8c46eb5f14345 to your computer and use it in GitHub Desktop.
Save guibou/84333621ff0e6f9374b8c46eb5f14345 to your computer and use it in GitHub Desktop.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
import GHC.Generics
import Data.Data (Data, Typeable)
data Tag = TagA | TagB
data MyGADT t where
A :: Int -> MyGADT TagA
B :: Float -> MyGADT TagB
deriving instance Show (MyGADT t)
deriving instance Typeable t => Data (MyGADT t)
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
import Data.Data
data Tag = TagA | TagB
data MyGADT t where
A :: Int -> MyGADT TagA
B :: Float -> MyGADT TagB
deriving instance Show (MyGADT t)
instance Typeable t => Data (MyGADT t) where
gfoldl k z (A i) = z (\a -> A a) `k` i
gfoldl k z (B f) = z (\a -> B a) `k` f
gunfold k z c = error "gunfold not implemented"
toConstr (A _) = con_A
toConstr (B _) = con_B
dataTypeOf _ = ty_T
con_A = mkConstr ty_T "A" [] Prefix
con_B = mkConstr ty_T "B" [] Prefix
ty_T = mkDataType "MyGADT" [con_A, con_B]
blu :: Data a => a -> [Int]
blu v = concat $ gmapQ f [v]
where
f :: forall a. (Data a, Typeable a) => a -> [Int]
f e = case cast @_ @Int e of
Just i -> [i]
_ -> concat $ gmapQ f e
data MyADT where
A' :: Int -> MyADT
B' :: Float -> MyADT
deriving (Data)
[1 of 1] Compiling Main ( GADTsData.hs, GADTsData.o )
GADTsData.hs:15:1: error:
• Couldn't match type ‘t’ with ‘'TagA’
Expected: c (MyGADT t)
Actual: c (MyGADT 'TagA)
‘t’ is a rigid type variable bound by
the instance declaration
at GADTsData.hs:15:1-47
• In the expression: k (z (\ a1 -> A a1))
In a case alternative: GHC.Types.I# 1# -> k (z (\ a1 -> A a1))
In the expression:
case Data.Data.constrIndex c of
GHC.Types.I# 1# -> k (z (\ a1 -> A a1))
_ -> k (z (\ a1 -> B a1))
When typechecking the code for ‘Data.Data.gunfold’
in a derived instance for ‘Data (MyGADT t)’:
To see the code I am typechecking, use -ddump-deriv
• Relevant bindings include
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Data.Data.Constr -> c (MyGADT t)
(bound at GADTsData.hs:15:1)
|
15 | deriving instance Typeable t => Data (MyGADT t)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment