Unhelpful inferred type in error message

[facundominguez]

The following program produces a verification error

module Test where

{-@ test :: [{i:_ | p i }] -> [{v:_ | q v && r v}] @-}
test :: [Int] -> [Int]
test xs = myid (cast xs)

{-@ assume cast :: [{i:Int| p i}] -> [{v:_ | q v}] @-}
cast :: [Int] -> [Int]
cast xs = xs

{-@ opaque-reflect p @-}
{-@ opaque-reflect q @-}
{-@ opaque-reflect r @-}

p :: Int -> Bool
p x = True

q :: Int -> Bool
q x = True

r :: Int -> Bool
r x = True

myid :: a -> a
myid x = x

Here's the error

Test.hs:6:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : GHC.Types.Int
    .
    is not a subtype of the required type
      VV : {VV##682 : GHC.Types.Int | Test.r VV##682}
    .
    Constraint id 3
  |
6 | test xs = myid (cast xs)
  | ^^^^^^^^^^^^^^^^^^^^^^^^

As can be seen the inferred type is bare Int, when the strongest type that we could hope to be inferred is {v:Int | q v}. Actually, this is the inferred type if we remove the call to myid.

This is a problem because LH is making very hard to identify what are the facts known about the inferred type. In a larger program it is tedious to reconstruct by trial an error how far LH went.

The constraint in question uses a kvar for the inferred type.

constraint:
  lhs {VV : int | [$k_##593[VV##592:=VV][VV##597:=VV##677][VV##682:=VV][VV##F:=VV][lq_tmp$x##591:=lq_anf$][lq_tmp$x##599:=VV][lq_tmp$x##602:=VV##677][lq_tmp$x##683:=VV]]}
  rhs {VV : int | [(Test.r VV)]}
  id 3 tag [7]
  // META constraint id 3 : Test.hs:5:1-24
  environment:
    // elided some likely irrelevant bindings
    
    lq_anf$ :
      {lq_tmp$x : [int] |
         [((GHC.Types_LHAssumptions.len lq_tmp$x) >= 0)]}
    
    _xs : {VV : [int] | [((GHC.Types_LHAssumptions.len VV) >= 0)]}

Verification would pass if we add

-{-@ assume cast :: [{i:Int| p i}] -> [{v:_ | q v}] @-}
+{-@ assume cast :: [{i:Int| p i}] -> [{v:_ | q v && r v}] @-}

or if we remove

-{-@ test :: [{i:_ | p i }] -> [{v:_ | q v && r v}] @-}
+{-@ test :: [{i:_ | p i }] -> [{v:_ | q v}] @-}

This issue is to discuss what could be done to enrich the inferred type.

[facundominguez]

The .fqout file has

$k_##593 := exists [VV##F##5 : int]. Test.q VV##F##5

Is this a matter of just substituting the kvar in the error message then?