detect (->) TyCon and substitute FunTy in WeakToCore

[coq-hetmet.git] / src / HaskWeakTypes.v

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 56c2f48..6b6b61e 100644 (file)
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -97,6 +97,7 @@ Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
 Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
   match wt with
     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
     | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
                                            | t1'             => AppTy t1' (weakTypeToCoreType' t2)