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