- coercionAxiom co =
- case isCoercionTyCon_maybe co of
- -- See Note [Newtype coercions] in
- -- types/TyCon
- Just (arity,coKindFun) | (l,r) <- (coKindFun $ map mkTyVarTy vs) ->
- -- Here we eta-expand the newtype coercion,
- -- which makes the ext-core typechecker somewhat simpler.
- (tyvars,mkAppTys l extraVs,mkAppTys r extraVs)
- where (vs, extraVs) = (take arity tyvars,
- map mkTyVarTy $ drop arity tyvars)
- Nothing -> pprPanic "MkExternalCore: coercion tcon lacks a kind fun"
- (ppr tcon)