36 | | (The type variables beginning with underscores are bound here and we add one underscore for each level of kinding.) |

| 36 | (The type variables beginning with underscores are bound here; we add one underscore for each level of kinding.) |

| 37 | |

| 38 | As an example, consider |

| 39 | {{{ |

| 40 | data T (f::*->*) = T1 (f Int) | T2 (f Bool) |

| 41 | }}} |

| 42 | The type of the conversion constructor is as follows (using more meaningful type variable names): |

| 43 | {{{ |

| 44 | tfTy (T::(*->*)->*) = |

| 45 | forall f f_CC. |

| 46 | (forall a a_CC. |

| 47 | (TF a a_CC) -> (TF (f a) (f_CC a_CC))) -> |

| 48 | TF (T f) (T_CC f_CC) |

| 49 | }}} |

| 50 | The conversion constructor might be implemented as |

| 51 | {{{ |

| 52 | tfT tff = TF toT frT |

| 53 | where |

| 54 | toT (T1 x) = T1 (to (tff tfInt ) x) |

| 55 | toT (T2 y) = T2 (to (tff tfBool) y) |

| 56 | frT (T1 x) = T1 (fr (tff tfInt ) x) |

| 57 | frT (T2 y) = T2 (fr (tff tfBool) y) |

| 58 | }}} |

| 59 | where `tfInt` and `tfBool` are the conversion constructors for `Int`s and `Bool`s. |