module spec GHC.ForeignPtr where

measure fplen :: GHC.ForeignPtr.ForeignPtr a -> GHC.Types.Int

type ForeignPtrV a   = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v}
type ForeignPtrN a N = {v: GHC.ForeignPtr.ForeignPtr a | 0 <= fplen v && fplen v == N }

mallocPlainForeignPtrBytes :: n:{v:GHC.Types.Int  | v >= 0 } -> (GHC.Types.IO (ForeignPtrN a n))