Generated function cannot be compiled by Coq (cannot infer type)

I have the following Haskell code. The case-expressions are necessary due to the bug in Malte's library...

type Stack = [Integer]
type Code  = [Op]
data Op    = PUSH Integer | ADD

execStrict2 :: Stack -> Code -> Stack
execStrict2 [] s = case s of
                     []           -> []
                     PUSH n : ops -> execStrict2 [n] ops
execStrict2 (c:cs) s = case s of
                         PUSH n : ops -> execStrict2 (n : c :cs) ops
execStrict2 (m:n:s') s = case s of
                         ADD : ops -> execStrict2 (n + m : s') ops

The generated Coq code then produces the following error when I try to compile it.

Error: Cannot infer ?T of type "Type" in the partial instance "Free Shape Pos (List Shape Pos ?T)" found for this placeholder of
type "Type" in environment:
Shape : Type
Pos : Shape -> Type
P : Partial Shape Pos