[ re #660 ] inline lets when detecting parameters

src/Core/Context/Data.idr

@@ -75,6 +75,8 @@ getConPs : {vars : _} ->
 getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
     = let bacc = getPs acc tyn ty in
           getConPs (map (map (map weaken)) bacc) tyn sc
+getConPs acc tyn (Bind _ x (Let _ _ v ty) sc)
+    = getConPs acc tyn (subst v sc)
 getConPs acc tyn tm = toPos (getPs acc tyn tm)
 
 paramPos : Name -> (dcons : List ClosedTerm) ->

tests/Main.idr

@@ -93,7 +93,7 @@ idrisTests
        -- Packages and ipkg files
        "pkg001", "pkg002", "pkg003", "pkg004", "pkg005",
        -- Positivity checking
-       "positivity001",
+       "positivity001", "positivity002",
        -- Larger programs arising from real usage. Typically things with
        -- interesting interactions between features
        "real001", "real002",

tests/idris2/positivity002/Issue660.idr

@@ -0,0 +1,11 @@
+module Issue660
+
+%default total
+
+%logging declare.data.parameters 20
+
+data C : Type -> Type where
+  MkC : List a -> C a
+
+data D : Type -> Type where
+  MkD : {0 a : Type} -> let 0 b = List a in b -> D a

tests/idris2/positivity002/expected

@@ -0,0 +1,3 @@
+1/1: Building Issue660 (Issue660.idr)
+LOG declare.data.parameters:20: Positions of parameters for datatypeIssue660.C: [0]
+LOG declare.data.parameters:20: Positions of parameters for datatypeIssue660.D: [0]

tests/idris2/positivity002/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 Issue660.idr --check
+
+rm -rf build