improve detection of type function kinds, mainly their saturation needs

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 0775229..f11e63b 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -64,13 +64,21 @@ errOrFail :: OrError t -> t
 errOrFail (OK x)    = x
 errOrFail (Error s) = Prelude.error s
 
+rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
+rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
+                  ,
+                   coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
+                   where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
+
 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
 tyConOrTyFun n =
    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
    then Prelude.Right n
    else if TyCon.isFamInstTyCon n
         then Prelude.Right n
-        else Prelude.Left n
+        else if TyCon.isSynTyCon n
+             then Prelude.Right n
+             else Prelude.Left n
 
 nat2int :: Nat -> Prelude.Int
 nat2int O     = 0

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 78223cf..ccd4973 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -29,6 +29,12 @@ Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant he
 Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
 Variable hetmet_csp_name    : CoreName.              Extract Inlined Constant hetmet_csp_name  => "PrelNames.hetmet_csp_name".
 
+Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
+  split_list lwt (length (fst (tyFunKind tf))) >>=
+  fun argsrest =>
+    let (args,rest) := argsrest in
+      OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
+
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with
   | TyVarTy  cv              => match coreVarToWeakVar cv with
@@ -45,7 +51,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                   | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
                                 end) lct)
       in match tyConOrTyFun tc_ with
-           | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
+           | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
            | inl tc => if eqd_dec tc ModalBoxTyCon
                          then match lct with
                                 | ((TyVarTy ec)::tbody::nil) =>

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d77d074..7dd93ad 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -142,7 +142,11 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
                       end
           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
-                          | nil    => Error "WTyFunApp applied to too many types"
+                          | nil    => Error ("WTyFunApp applied to too many types"(* +++ eol +++
+                                             "  tyCon= "           +++ toString tc +++ eol +++
+                                             "  tyConKindArgs= "   +++ toString (fst (tyFunKind tc)) +++ eol +++
+                                             "  tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
+                                             "  types= "           +++ toString lt +++ eol*))
                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
                                         let case_weakTypeListToTypeList := tt in _
                         end
@@ -166,7 +170,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
       try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
         subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
       apply (Error ("Kind mismatch in WAppTy: "+++err)).
-   
+
   destruct case_weakTypeListToTypeList.
     apply (addErrorMessage "case_weakTypeListToTypeList").
     destruct t' as [ k' t' ].

diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v
index 896aff4..3fb7a4b 100644 (file)
--- a/src/HaskWeakVars.v
+++ b/src/HaskWeakVars.v
@@ -49,10 +49,10 @@ Definition tyConTyVars (tc:CoreTyCon) :=
   Opaque tyConTyVars.
 Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).
 
-Variable rawTyFunKind : CoreTyCon -> Kind. Extract Inlined Constant rawTyFunKind => "(coreKindToKind . TyCon.tyConKind)".
+Variable rawTyFunKind : CoreTyCon -> ((list Kind) * Kind). Extract Inlined Constant rawTyFunKind => "rawTyFunKind".
 
 Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) :=
-  splitKind (rawTyFunKind tc).
+  rawTyFunKind tc.
 
 Instance WeakVarToString : ToString WeakVar :=
   { toString := fun x => toString (weakVarToCoreVar x) }.