168 | | * representation |

| 168 | The internal representation of GADTs is as regular algebraic datatypes that carry coercion evidence as arguments. A declaration like |

| 169 | {{{ |

| 170 | data T a b where |

| 171 | T1 :: a -> b -> T [a] (a,b) |

| 172 | }}} |

| 173 | would result in a data constructor with type |

| 174 | {{{ |

| 175 | T1 :: forall a b. forall a1 b1. (a :=: [a1], b :=: (a1, b1)) => a1 -> b1 -> T a b |

| 176 | }}} |

| 177 | This means that (unlike in the previous intermediate language) all data constructor return types have the form `T a1 ... an` where |

| 178 | `a1` through `an` are the parameters of the datatype. |

| 179 | |

| 180 | However, we also generate wrappers for GADT data constructors which have the expected user-defined type, in this case |

| 181 | {{{ |

| 182 | $wT1 = /\a b. \x y. T1 [a] (a,b) a b [a] (a,b) x y |

| 183 | }}} |

| 184 | Where the 4th and 5th arguments given to `T1` are the reflexive coercions |

| 185 | {{{ |

| 186 | [a] :: [a] :=: [a] |

| 187 | (a,b) :: (a,b) :=: (a,b) |

| 188 | }}} |