Cannot infer type for partially applied function
I have the following Haskell code.
module FunProp where
import Test.QuickCheck
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs
f :: [a] -> [a]
f = map id
id :: a -> a
id x = x
map_id :: Property
map_id = map id === id
f_prop :: Property
f_prop = f === id
The module is then translated Coq without any problems with regard to the tool. However, the theorems for map_id
and f_prop
cannot be loaded as Coq cannot infer their types.
Theorem map_id : forall (Shape : Type) (Pos : Shape -> Type),
pure (fun x_0 => map Shape Pos (pure (fun x_1 => id Shape Pos x_1)) x_0) =
pure (fun x_1 => id Shape Pos x_1).
Proof.
(* FILL IN HERE *)
Admitted.
Theorem f_prop : forall (Shape : Type) (Pos : Shape -> Type),
f Shape Pos = pure (fun x_0 => id Shape Pos x_0).
Proof.
(* FILL IN HERE *)
Admitted.