Positivity checking rejects otherwise accepted expression if they are encapsulated in a datatype or a record

[UlfNorell]

From sble...@gmail.com on November 29, 2013 14:31:49

Code (or the attached file if you don't want to have to copy/paste).

module positivity where

{- using functions: accepted! -}

AppFun : (F : Set → Set) (A : Set) → Set AppFun F A = F (F A)

data ExprFun (A : Set) : Set where con : (fa : AppFun ExprFun A) → ExprFun A

{- using datatypes: fails -}

data AppDat (F : Set → Set) (A : Set) : Set where appDat : F (F A) → AppDat F A

data ExprDat (A : Set) : Set where con : (fa : AppDat ExprDat A) → ExprDat A

{- using record: fails -}

record AppRec (F : Set → Set) (A : Set) : Set where field appRec : F (F A)

data ExprRec (A : Set) : Set where con : (fa : AppRec ExprRec A) → ExprRec A

Attachment: positivity.agda

Original issue: http://code.google.com/p/agda/issues/detail?id=984

[UlfNorell]

From ulf.nor...@gmail.com on November 29, 2013 07:39:16

The difference is that the definition of AppFun is inlined before positivity checking. If you define it like this instead it doesn't work:

data Top : Set where tt : Top

AppFun : (F : Set → Set) (A : Set) → Top → Set AppFun F A tt = F (F A)

data ExprFun (A : Set) : Set where con : (x : Top)(fa : AppFun ExprFun A x) → ExprFun A

Actually making this work without inlining would require tracking a lot more polarity information and probably some user annotations (like saying that AppDat takes a covariant functor).

Status: WontFix

[UlfNorell]

From andreas....@gmail.com on November 29, 2013 07:41:41

Which you can do in MiniAgda and at some time in the future should also be able to do in Agda.
But no plans to change this right now.

Labels: Type-Enhancement Positivity