| 1 | = A Proposal for using GADTs within the implementation of Template Haskell = |
| 2 | |
| 3 | == The problem == |
| 4 | |
| 5 | Haskell declarations and pragmas can appear in a variety of contexts, but not all declarations/pragmas can appear in all contexts. For examples, data declarations can appear only at top level; type family instances can appear at top-level, in classes (as defaults), and in instances, but never in `let`/`where` blocks; fixity declarations can be used anywhere other than in an instance declaration; etc. Yet, the Template Haskell `Dec` type monolithically includes ''all'' possible declarations. Currently, consumers of `Dec`s need to eliminate the possibility of `Dec`s in various contexts by emitting errors. Many users of Template Haskell might not know the intricate details of where which declarations can appear, making these "impossible" scenarios error-prone. And, with the solutions to #8100 (adding standalone-deriving) and #9064 (adding `default` type signatures to class declarations), the problem gets worse. |
| 6 | |
| 7 | == A proposed solution == |
| 8 | |
| 9 | Use the type system to track which declaration form can be used where. First, declare |
| 10 | |
| 11 | {{{ |
| 12 | data InTopLevel = YesInTopLevel | NoInTopLevel deriving Typeable |
| 13 | data InClass = YesInClass | NoInClass deriving Typeable |
| 14 | data InInstance = YesInInstance | NoInInstance deriving Typeable |
| 15 | data InLet = YesInLet | NoInLet deriving Typeable |
| 16 | }}} |
| 17 | |
| 18 | These are all Boolean-like flags with more perspicuous names. |
| 19 | |
| 20 | Then, pack these flags into a type: |
| 21 | |
| 22 | {{{ |
| 23 | data DecContext = DC InTopLevel InClass InInstance InLet deriving Typeable |
| 24 | }}} |
| 25 | |
| 26 | Now, define `Dec` as a GADT indexed by `DecContext`: |
| 27 | |
| 28 | {{{ |
| 29 | data Dec :: DecContext -> * where |
| 30 | FunD :: Name -> [Clause] -> Dec (DC top NoInClass inst lt) |
| 31 | -- ^ @{ f p1 p2 = b where decs }@ |
| 32 | ValD :: Pat -> Body -> [LetDec] -> Dec (DC top NoInClass inst lt) |
| 33 | -- ^ @{ p = b where decs }@ |
| 34 | DataD :: Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] |
| 35 | -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 36 | -- ^ @{ data Cxt x => T x = A x | B (T x) |
| 37 | -- deriving (Z,W)}@ |
| 38 | NewtypeD :: Cxt -> Name -> [TyVarBndr] -> Con -> [Name] |
| 39 | -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 40 | -- ^ @{ newtype Cxt x => T x = A (B x) |
| 41 | -- deriving (Z,W)}@ |
| 42 | TySynD :: Name -> [TyVarBndr] -> Type -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 43 | -- ^ @{ type T x = (x,x) }@ |
| 44 | ClassD :: Cxt -> Name -> [TyVarBndr] -> [FunDep] -> [ClassDec] |
| 45 | -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 46 | -- ^ @{ class Eq a => Ord a where ds }@ |
| 47 | InstanceD :: Cxt -> Type -> [InstanceDec] -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 48 | -- ^ @{ instance Show w => Show [w] |
| 49 | -- where ds }@ |
| 50 | SigD :: Name -> Type -> Dec (DC top cls inst lt) |
| 51 | -- ^ @{ length :: [a] -> Int }@ |
| 52 | ForeignD :: Foreign -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 53 | -- ^ @{ foreign import ... } |
| 54 | -- { foreign export ... }@ |
| 55 | |
| 56 | InfixD :: Fixity -> Name -> Dec (DC top cls NoInInstance lt) |
| 57 | -- ^ @{ infix 3 foo }@ |
| 58 | |
| 59 | -- | pragmas |
| 60 | PragmaD :: Pragma loc -> Dec loc |
| 61 | -- ^ @{ {\-# INLINE [1] foo #-\} }@ |
| 62 | |
| 63 | -- | type families (may also appear in [Dec] of 'ClassD' and 'InstanceD') |
| 64 | FamilyD :: FamFlavour -> Name -> [TyVarBndr] -> Maybe Kind |
| 65 | -> Dec (DC top cls NoInInstance NoInLet) |
| 66 | -- ^ @{ type family T a b c :: * }@ |
| 67 | |
| 68 | DataInstD :: Cxt -> Name -> [Type] -> [Con] -> [Name] |
| 69 | -> Dec (DC top NoInClass inst NoInLet) |
| 70 | -- ^ @{ data instance Cxt x => T [x] = A x |
| 71 | -- | B (T x) |
| 72 | -- deriving (Z,W)}@ |
| 73 | NewtypeInstD :: Cxt -> Name -> [Type] -> Con -> [Name] |
| 74 | -> Dec (DC top NoInClass inst NoInLet) |
| 75 | -- ^ @{ newtype instance Cxt x => T [x] = A (B x) |
| 76 | -- deriving (Z,W)}@ |
| 77 | TySynInstD :: Name -> TySynEqn -> Dec (DC top cls inst NoInLet) |
| 78 | -- ^ @{ type instance ... }@ |
| 79 | |
| 80 | ClosedTypeFamilyD :: Name -> [TyVarBndr] -> Maybe Kind -> [TySynEqn] |
| 81 | -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 82 | -- ^ @{ type family F a b :: * where ... }@ |
| 83 | |
| 84 | RoleAnnotD :: Name -> [Role] -> Dec (DC top NoInClass NoInInstance NoInLet) |
| 85 | -- ^ @{ type role T nominal representational }@ |
| 86 | }}} |
| 87 | |
| 88 | Each constructor's return type tells you where the declaration is prohibited. |
| 89 | |
| 90 | Then, specialize `Dec` to the four cases that exist: |
| 91 | |
| 92 | {{{ |
| 93 | type TopLevelDec = Dec (DC YesInTopLevel NoInClass NoInInstance NoInLet) |
| 94 | type ClassDec = Dec (DC NoInTopLevel YesInClass NoInInstance NoInLet) |
| 95 | type InstanceDec = Dec (DC NoInTopLevel NoInClass YesInInstance NoInLet) |
| 96 | type LetDec = Dec (DC NoInTopLevel NoInClass NoInInstance YesInLet) |
| 97 | }}} |
| 98 | |
| 99 | And now, we can use these last 4 types as simple datatypes that have fewer constructors than the full `Dec` type. Types to the rescue! |
| 100 | |
| 101 | For example: |
| 102 | {{{ |
| 103 | data Clause = Clause [Pat] Body [LetDec] |
| 104 | -- ^ @f { p1 p2 = body where decs }@ |
| 105 | deriving( Show, Eq, Data, Typeable, Generic ) |
| 106 | }}} |
| 107 | |
| 108 | The `[LetDec]` is the `where` stanza of a declaration. Or: |
| 109 | |
| 110 | {{{ |
| 111 | data Exp |
| 112 | = ... |
| 113 | | LetE [LetDec] Exp -- ^ @{ let x=e1; y=e2 in e3 }@ |
| 114 | | ... |
| 115 | deriving( Show, Eq, Data, Typeable, Generic ) |
| 116 | }}} |
| 117 | |
| 118 | Here, we include only `LetDec`s in a `let`. You can see above that `ClassDec` and `InstanceDec` are used as appropriate in `Dec`. |
| 119 | |
| 120 | Under this scenario, `[d| ... |]` would have the type `Q [TopLevelDec]`, and if you have a top-level splice, it must also be of type `Q [TopLevelDec]`. |
| 121 | |
| 122 | `Pragma`, which are similarly sometimes available and sometimes unavailable, depending on context, are similarly indexed: |
| 123 | |
| 124 | {{{ |
| 125 | data Pragma :: DecContext -> * where |
| 126 | InlineP :: Name -> Inline -> RuleMatch -> Phases |
| 127 | -> Pragma (DC top cls inst lt) |
| 128 | SpecialiseP :: Name -> Type -> Maybe Inline -> Phases |
| 129 | -> Pragma (DC top NoInClass inst lt) |
| 130 | SpecialiseInstP :: Type -> Pragma (DC NoInTopLevel NoInClass inst NoInLet) |
| 131 | RuleP :: String -> [RuleBndr] -> Exp -> Exp -> Phases |
| 132 | -> Pragma (DC top NoInClass NoInInstance NoInLet) |
| 133 | AnnP :: AnnTarget -> Exp -> Pragma (DC top NoInClass NoInInstance NoInLet) |
| 134 | LineP :: Int -> String -> Pragma (DC top NoInClass NoInInstance NoInLet) |
| 135 | }}} |
| 136 | |
| 137 | == Discussion == |
| 138 | |
| 139 | === Pros === |
| 140 | |
| 141 | This seems to work, in preliminary tests. Matching on this GADT does not trigger #3927 (that is, it does not warn about vacuous incomplete patterns), and you can't squeeze, say, a `DataD` into a `LetDec`. |
| 142 | |
| 143 | === Cons === |
| 144 | |
| 145 | * `Data` and `Generic` (see #9527, requesting `Generic` instances) don't play well with GADTs. I can hand-write `Data` instances for `Dec` and `Pragma`, but these implement only `gfoldl` and error on `gunfold`. I have not yet tried to write hand-written `Generic` instances, but I'm not hopeful. |
| 146 | |
| 147 | * I frequently use `:info Dec` in GHCi when writing TH code. The output after this transformation is much noisier than it was before. |
| 148 | |
| 149 | == Questions == |
| 150 | |
| 151 | * Does anyone use `gunfold` for TH types? |
| 152 | |
| 153 | * Is there a need for `Generic` instances for `Dec` and `Pragma`? Are these possible for GADTs? |