Name resolution chokes on dependent pairs + type aliases

[AlecsFerra]

import Language.Haskell.Liquid.ProofCombinators
-- {-@ type Ix ty R = { val:ty | prop val = R @-}

{-@ foo :: (v::Int, { r:Int | r = v }) @-}
foo :: (Int, Int)
foo = (3, 3)


{-@ bar :: (v::Int, Ix Int v) @-}
bar :: (Int, Int)
bar = (3, 3)

Gives the following error:

    Unknown logic name `v`
    Cannot resolve name
    Maybe you meant one of: snd len fst Max Min
   |
13 | {-@ bar :: (v::Int, Ix Int v) @-}

[AlecsFerra]

exprArgs should also do something with contexts apparently when we transform types to expressions

[facundominguez]

resolveLogicNames calls to emapSpecM, which computes the local variables at each location. As I understand it, v in this example is a local variable bound by v :: Int. However, it doesn't seem to be picked by emapSpecM.

The line that produces the error is

liquidhaskell/liquidhaskell-boot/src/Language/Haskell/Liquid/LHNameResolution.hs

Line 828 in 1695e59

addError $ errResolve alts "logic name" "Cannot resolve name" ls

inside resolveLogicName, where ss should hold the local variables. In the failure case, ss is the empty list. I'm conjecturing that it could be a mistake, and that it should be made to contain v.

[AlecsFerra]

I was able to move the error to fixpoint in here apparenty now is the constraint generation failing

[AlecsFerra]

It looks like dependent pairs are just super broken

[AlecsFerra]

Oh now it shows the right error the abstract refinement is inlined wrong

TestSKI.hs:7:12: error:
    Illegal type specification for `SKILam.bar`
    SKILam.bar :: k:GHC.Types.Int -> (GHC.Types.Bool, {VV##0 : GHC.Types.Int | m})<\m VV -> {VV##0 : GHC.Types.Int | m}>
    Sort Error in Refinement: {VV##0 : int | m}
    Unbound symbol m --- perhaps you meant: k ?
    Just
  |
7 | {-@ bar :: k:Int -> (m::Bool, A m) @-}
  |            ^^^^^^^^^^^^^^^^^^^^^^^^

Should only appear in the abstract refinement not in the type of the second component