Reflection weakens higher order reasoning #2579
Description
The below is SAFE without the reflection flag:
{-@ type ListN a N = {v:[a] | len v = N} @-}
{-@ foldl' :: l:Nat
-> (ListN a l -> ListN a l -> ListN a l)
-> ListN a l -> [ListN a l] -> ListN a l @-}
foldl' :: Int -> ([a] -> [a] -> [a]) -> [a] -> [[a]] -> [a]
foldl' ins f acc xs = foldl f acc xs
But with the reflection flag it creates the below error:
**** LIQUID: UNSAFE (3 constraints checked) ************************************
tests/pos/fixme.hs:11:1: error:
Liquid Type Mismatch
.
The inferred type
VV : {v : [a] | v == GHC.Internal.Data.Foldable.foldl f##aDg acc##aDh xs##aDi
&& GHC.Types_LHAssumptions.len v >= 0}
.
is not a subtype of the required type
VV : {VV##1197 : [a] | GHC.Types_LHAssumptions.len VV##1197 == ins##aDf}
.
in the context
xs##aDi : {v : [[a]] | GHC.Types_LHAssumptions.len v >= 0}
acc##aDh : {acc##aDh : [a] | GHC.Types_LHAssumptions.len acc##aDh == ins##aDf
&& GHC.Types_LHAssumptions.len acc##aDh >= 0}
ins##aDf : {ins##aDf : GHC.Types.Int | ins##aDf >= 0}
Constraint id 2
|
11 | foldl' ins f acc xs = foldl f acc xs
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
tests/pos/fixme.hs:11:29: error:
Liquid Type Mismatch
.
The inferred type
VV : {v : [a] | GHC.Types_LHAssumptions.len v >= 0}
.
is not a subtype of the required type
VV : {VV##1241 : [a] | GHC.Types_LHAssumptions.len VV##1241 == ins##aDf}
.
in the context
xs##aDi : {v : [[a]] | GHC.Types_LHAssumptions.len v >= 0}
acc##aDh : {acc##aDh : [a] | GHC.Types_LHAssumptions.len acc##aDh == ins##aDf
&& GHC.Types_LHAssumptions.len acc##aDh >= 0}
ins##aDf : {ins##aDf : GHC.Types.Int | ins##aDf >= 0}
Constraint id 9
|
11 | foldl' ins f acc xs = foldl f acc xs