- do k1 <- ch t1
- k2 <- ch t2
- case k1 of
- Karrow k11 k12 ->
- do require (k2 `subKindOf` k11)
- ("kinds don't match in type application: " ++ show t ++ "\n" ++
- "operator kind: " ++ show k11 ++ "\n" ++
- "operand kind: " ++ show k2)
- return k12
- _ -> fail ("applied type has non-arrow kind: " ++ show t)
+ case splitTyConApp_maybe t of
+ Just (tc, tys) -> do
+ tcK <- qlookupM tcenv_ tcenv eempty tc
+ case tcK of
+ Kind _ -> checkTapp t1 t2
+ Coercion (DefinedCoercion tbs (from,to)) -> do
+ -- makes sure coercion is fully applied
+ require (length tys == length tbs) $
+ ("Arity mismatch in coercion app: " ++ show t)
+ let (tvs, tks) = unzip tbs
+ argKs <- mapM (checkTy es) tys
+ require (all (uncurry eqKind) (zip tks argKs))
+ ("Kind mismatch in coercion app: " ++ show tks
+ ++ " and " ++ show argKs ++ " t = " ++ show t)
+ return $ Keq (substl tvs tys from) (substl tvs tys to)
+ Nothing -> checkTapp t1 t2
+ where checkTapp t1 t2 = do
+ k1 <- ch t1
+ k2 <- ch t2
+ case k1 of
+ Karrow k11 k12 ->
+ case k2 of
+ Keq eqTy1 eqTy2 -> do
+ -- Distribute the type operator over the
+ -- coercion
+ subK1 <- checkTy es eqTy1
+ subK2 <- checkTy es eqTy2
+ require (subK2 `subKindOf` k11 &&
+ subK1 `subKindOf` k11) $
+ kindError
+ return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2)
+ _ -> do
+ require (k2 `subKindOf` k11) kindError
+ return k12
+ where kindError =
+ "kinds don't match in type application: "
+ ++ show t ++ "\n" ++
+ "operator kind: " ++ show k11 ++ "\n" ++
+ "operand kind: " ++ show k2
+ _ -> fail ("applied type has non-arrow kind: " ++ show t)
+