Translated data types violate Coq's strict positivity restriction

[MajaRet]

Description

Some data types are translated into Coq data types that violate the strict positivity restriction. As a result, the generated Coq code cannot be compiled.

Steps to Reproduce

Translate the following Haskell program with the Free compiler.

data NSP a = Val a | Stack (NSP (NSP a))

Expected Behavior

The compiler should throw an error when it encounters a Haskell data type whose translation would violate the strict positivity restriction.

Actual Behavior

No error is thrown. Translating this program leads to the following data type definition in Coq.

Inductive NSP (Shape : Type) (Pos : Shape -> Type) (a : Type) : Type
  := val : Free Shape Pos a -> NSP Shape Pos a
  |  stack : Free Shape Pos (NSP Shape Pos (NSP Shape Pos a)) -> NSP Shape Pos a.

This definition causes the following error.

Non strictly positive occurrence of 
"NSP" in
 "Free Shape Pos (NSP Shape Pos (NSP Shape Pos a)) ->
  NSP Shape Pos a".

Versions

• Git commit: 8779013877645b9547bb36c93fa1df9856b2b1aa
• ghc --version: 8.6.5
• cabal --version: 3.2.0.0
• coqc --version: 8.11.0
• OS: Ubuntu 19.10

ToDo

Implement an analysis that checks whether a data type's translation would violate the strict positivity restriction and throw an error if this is the case.