@@ -33,10 +33,8 @@ interpFTy (FAny t) = t
33interpFTy FUnit = ()
33interpFTy FUnit = ()
35ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
35ForeignTy : (xs:List FTy) -> (t:FTy) -> Type
36−ForeignTy xs t = mkForeign' (reverse xs) (IO (interpFTy t)) where
36+ForeignTy Nil rt = IO (interpFTy rt)
37− mkForeign' : List FTy -> Type -> Type
37+ForeignTy (t::ts) rt = interpFTy t -> ForeignTy ts rt
38− mkForeign' Nil ty = ty
39− mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)
42data Foreign : Type -> Type where
40data Foreign : Type -> Type where