X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtraction-prefix.hs;fp=src%2FExtraction-prefix.hs;h=f11e63b20d773bf006a9a2273083bb486aa228dd;hp=0775229ddcebba6900626f7480da5dfbdec05e3d;hb=38e0c88fa03d930293f980681fa34a667402a20d;hpb=e1c9b2e7a28fabb4c0a9ce3cbd4d2ae099d60b5a

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 0775229..f11e63b 100644
--- 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