- in if (isFamilyTyCon tc)
- then recurse >>= fun recurse' => OK (WTyFunApp tc recurse')
- else if eqd_dec tc ModalBoxTyCon
- then match lct with
- | ((TyVarTy ec)::tbody::nil) =>
- match coreVarToWeakVar ec with
- | WTypeVar ec' => coreTypeToWeakType tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
- | WExprVar _ => Error "encountered expression variable in a modal box type"
- | WCoerVar _ => Error "encountered coercion variable in a modal box type"
- end
- | _ => Error "mis-applied modal box tycon"
- end
- else let tc' := if eqd_dec tc ArrowTyCon
- then WFunTyCon
- else WTyCon tc
- in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
- | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType t1 >>= fun t1' =>
- coreTypeToWeakType t2 >>= fun t2' =>
- coreTypeToWeakType t3 >>= fun t3' =>
+ in match tyConOrTyFun tc_ with
+ | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
+ | inl tc => if eqd_dec tc ModalBoxTyCon
+ then match lct with
+ | ((TyVarTy ec)::tbody::nil) =>
+ match coreVarToWeakVar ec with
+ | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
+ | WExprVar _ => Error "encountered expression variable in a modal box type"
+ | WCoerVar _ => Error "encountered coercion variable in a modal box type"
+ end
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
+ end
+ else let tc' := if eqd_dec tc ArrowTyCon
+ then WFunTyCon
+ else WTyCon tc
+ in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
+ end
+ | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
+ coreTypeToWeakType' t2 >>= fun t2' =>
+ coreTypeToWeakType' t3 >>= fun t3' =>