5 | | With promotion, the situation is murkier. If I understand correctly, `CoercionTy` embeds coercions in types, so in principle it should be possible to end up with a type that refers to a coercion explicitly, when you promote a GADT. However, I haven't tried too hard to find an example source program where this happens. goldfire, perhaps you would know? I can probably turn it into a panic with GHC HEAD. |

| 5 | With promotion, this is not true: |

| 6 | |

| 7 | {{{ |

| 8 | {-# LANGUAGE TypeFamilies #-} |

| 9 | {-# LANGUAGE Rank2Types #-} |

| 10 | {-# LANGUAGE TypeInType #-} |

| 11 | unit p where |

| 12 | signature A where |

| 13 | import GHC.Types |

| 14 | type family F a where |

| 15 | F Bool = Type |

| 16 | module B where |

| 17 | import A |

| 18 | foo :: forall (a :: F Bool). a -> a |

| 19 | foo x = x |

| 20 | unit q where |

| 21 | dependency p[A=<A>] |

| 22 | module C where |

| 23 | import B |

| 24 | }}} |