GHC 9.14 support

[gergoerdi]

This draft PR adds GHC 9.14 support. It is a draft because I haven't gone through the trouble of factoring out the compatibility parts so now it only builds with GHC 9.14.

The more pertinent reason that I am making this PR in this state is because there are two mysterious (to me) test failures on the branch:

ple-pos

ple/pos/SKIIdx.hs:195:3: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : SKIIdx.Comb | v == SKIIdx.I σ##a1SZ γ##a1T3
                              && Language.Haskell.Liquid.ProofCombinators.prop v == GHC.Internal.Tuple.(,,) γ##a1T3 (SKIIdx.iType σ##a1SZ) (SKIIdx.makeId σ##a1SZ γ##a1T3)
                              && SKIIdx.I##lqdc##$select##SKIIdx.I##1 v == σ##a1SZ
                              && SKIIdx.I##lqdc##$select##SKIIdx.I##2 v == γ##a1T3}
    .
    is not a subtype of the required type
      VV : {VV##8356 : SKIIdx.Comb | Language.Haskell.Liquid.ProofCombinators.prop VV##8356 == GHC.Internal.Tuple.(,,) γ##a1T3 (SKIIdx.Arrow σ##a1SZ τ##a1T1) (SKIIdx.makeBracketing σ##a1SZ τ##a1T1 γ##a1T3 f##a1T5)}
    .
    in the context
      ?g : {?g : SKIIdx.Comb | ?g == ?a
                               && ?g == SKIIdx.CVar ?b ?c ?d
                               && Language.Haskell.Liquid.ProofCombinators.prop ?g == GHC.Internal.Tuple.(,,) ?c ?b (SKIIdx.lookupRef ?b ?c ?d)
                               && Language.Haskell.Liquid.ProofCombinators.prop ?g == GHC.Internal.Tuple.(,,) (SKIIdx.Cons σ##a1SZ γ##a1T3) τ##a1T1 f##a1T5
                               && SKIIdx.CVar##lqdc##$select##SKIIdx.CVar##1 ?g == ?b
                               && SKIIdx.CVar##lqdc##$select##SKIIdx.CVar##2 ?g == ?c
                               && SKIIdx.CVar##lqdc##$select##SKIIdx.CVar##3 ?g == ?d}
       
      γ##a1T3 : (SKIIdx.List SKIIdx.Ty)
       
      ?d : {?d : SKIIdx.Ref | Language.Haskell.Liquid.ProofCombinators.prop ?d == GHC.Internal.Tuple.(,) ?b ?c}
       
      σ##a1SZ : SKIIdx.Ty
       
      ?f : (SKIIdx.List SKIIdx.Ty)
       
      τ##a1T1 : SKIIdx.Ty
       
      ?c : (SKIIdx.List SKIIdx.Ty)
       
      ?h : {?h : SKIIdx.Ref | ?h == ?d
                              && ?h == SKIIdx.Here ?e ?f
                              && Language.Haskell.Liquid.ProofCombinators.prop ?h == GHC.Internal.Tuple.(,) ?b ?c
                              && Language.Haskell.Liquid.ProofCombinators.prop ?h == GHC.Internal.Tuple.(,) ?e (SKIIdx.Cons ?e ?f)
                              && SKIIdx.Here##lqdc##$select##SKIIdx.Here##1 ?h == ?e
                              && SKIIdx.Here##lqdc##$select##SKIIdx.Here##2 ?h == ?f}
       
      ?a : {?a : SKIIdx.Comb | Language.Haskell.Liquid.ProofCombinators.prop ?a == GHC.Internal.Tuple.(,,) (SKIIdx.Cons σ##a1SZ γ##a1T3) τ##a1T1 f##a1T5}
       
      ?b : SKIIdx.Ty
       
      ?e : SKIIdx.Ty
    Constraint id 80
    |
195 |   I σ γ
    |   ^^^^^

[48 of 69] Compiling SKILam           ( ple/pos/SKILam.hs, /home/cactus/prog/haskell/liquid-haskell/import/liquidhaskell/dist-newstyle/build/x86_64-linux/ghc-9.14.1/tests-0.1.0.0/x/ple-pos/build/ple-pos/ple-pos-tmp/SKILam.o )
ple/pos/SKILam.hs:210:3: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : SKILam.Comb | v == SKILam.I σ##a1SY γ##a1T2
                              && Language.Haskell.Liquid.ProofCombinators.prop v == SKILam.Comb γ##a1T2 (SKILam.iType σ##a1SY) (SKILam.makeId σ##a1SY γ##a1T2)
                              && SKILam.I##lqdc##$select##SKILam.I##1 v == σ##a1SY
                              && SKILam.I##lqdc##$select##SKILam.I##2 v == γ##a1T2}
    .
    is not a subtype of the required type
      VV : {VV##9596 : SKILam.Comb | Language.Haskell.Liquid.ProofCombinators.prop VV##9596 == SKILam.Comb γ##a1T2 (SKILam.Arrow σ##a1SY τ##a1T0) (SKILam.makeBracketing σ##a1SY τ##a1T0 γ##a1T2 f##a1T4)}
    .
    in the context
      ?g : {?g : SKILam.Comb | ?g == ?a
                               && ?g == SKILam.CVar ?b ?c ?d
                               && Language.Haskell.Liquid.ProofCombinators.prop ?g == SKILam.Comb ?c ?b (SKILam.lookupRef ?b ?c ?d)
                               && Language.Haskell.Liquid.ProofCombinators.prop ?g == SKILam.Comb (SKILam.Cons σ##a1SY γ##a1T2) τ##a1T0 f##a1T4
                               && SKILam.CVar##lqdc##$select##SKILam.CVar##1 ?g == ?b
                               && SKILam.CVar##lqdc##$select##SKILam.CVar##2 ?g == ?c
                               && SKILam.CVar##lqdc##$select##SKILam.CVar##3 ?g == ?d}
       
      ?d : {?d : SKILam.Ref | Language.Haskell.Liquid.ProofCombinators.prop ?d == SKILam.Ref ?b ?c}
       
      σ##a1SY : SKILam.Ty
       
      ?f : (SKILam.List SKILam.Ty)
       
      τ##a1T0 : SKILam.Ty
       
      ?c : (SKILam.List SKILam.Ty)
       
      ?h : {?h : SKILam.Ref | ?h == ?d
                              && ?h == SKILam.Here ?e ?f
                              && Language.Haskell.Liquid.ProofCombinators.prop ?h == SKILam.Ref ?b ?c
                              && Language.Haskell.Liquid.ProofCombinators.prop ?h == SKILam.Ref ?e (SKILam.Cons ?e ?f)
                              && SKILam.Here##lqdc##$select##SKILam.Here##1 ?h == ?e
                              && SKILam.Here##lqdc##$select##SKILam.Here##2 ?h == ?f}
       
      ?a : {?a : SKILam.Comb | Language.Haskell.Liquid.ProofCombinators.prop ?a == SKILam.Comb (SKILam.Cons σ##a1SY γ##a1T2) τ##a1T0 f##a1T4}
       
      ?b : SKILam.Ty
       
      γ##a1T2 : (SKILam.List SKILam.Ty)
       
      ?e : SKILam.Ty
    Constraint id 98
    |
210 |   I σ γ
    |   ^^^^^

benchmark-icfp15-pos

[12 of 18] Compiling Incr             ( benchmarks/icfp15/pos/Incr.hs, /home/cactus/prog/haskell/liquid-haskell/import/liquidhaskell/dist-newstyle/build/x86_64-linux/ghc-9.14.1/tests-0.1.0.0/x/benchmark-icfp15-pos/build/benchmark-icfp15-pos/benchmark-icfp15-pos-tmp/Incr.o )
<no location info>: error:
    
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
subst: EXISTS (without disjoint binds)([("subst$subst$w##0##0",FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False})))],[lq_rnm$x##265:=subst$subst$subst$lq_rnm$x##265##0##0##0][subst$w##0:=subst$subst$subst$w##0##0##0][w:=subst$subst$w##0##0][w2:=subst$w2##0],PAnd [PAtom Eq (ECst (EVar "subst$subst$w##0##0") (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False})))) (ECst (EVar "subst$w##0") (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False})))),PAtom Eq (ECst (EVar "w##a1vV") (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False})))) (ECst (EVar "subst$subst$w##0##0") (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False})))),PAtom Ge (ECst (EApp (EApp (ECst (EVar "apply") (FFunc (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))) FInt)) (ECst (EVar "Incr.counter") (FFunc (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))) FInt))) (ECst (EVar "subst$subst$w##0##0") (FTC (TC "RIO.World" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))))) FInt) (ECon (I 0))])
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************

[facundominguez]

Thanks @gergoerdi! I'm stuck at the same point, roughly. I don't have the failure on Incr though. I think I fixed that one in 5a6b33e2d, merged in ucsd-progsys/liquid-fixpoint#819 and #2609.

I'll let you know if I discover what's making a difference for SKIIdx and SKILam.

[facundominguez]

This fixes the failing tests:

diff --git a/tests/ple/pos/SKIIdx.hs b/tests/ple/pos/SKIIdx.hs
index de8273324..48c608fb2 100644
--- a/tests/ple/pos/SKIIdx.hs
+++ b/tests/ple/pos/SKIIdx.hs
@@ -11,7 +11,13 @@ import Prelude
 
 import Language.Haskell.Liquid.ProofCombinators
 
-{-@ reflect id @-}
-{-@ reflect $  @-}
+{-@ assume reflect id as myId @-}
+
+{-@ reflect myId @-}
+myId :: a -> a
+myId x = x
 
 data List a = Nil | Cons a (List a)
diff --git a/tests/ple/pos/SKILam.hs b/tests/ple/pos/SKILam.hs
index 07496bda2..8e8970ea5 100644
--- a/tests/ple/pos/SKILam.hs
+++ b/tests/ple/pos/SKILam.hs
@@ -13,7 +13,13 @@ import Prelude
 
 import Language.Haskell.Liquid.ProofCombinators 
 
-{-@ reflect id @-}
-{-@ reflect $  @-}
+{-@ assume reflect id as myId @-}
+
+{-@ reflect myId @-}
+myId :: a -> a
+myId x = x
 
 data List a = Nil | Cons a (List a)

[facundominguez]

It is a draft because I haven't gone through the trouble of factoring out the compatibility parts so now it only builds with GHC 9.14

The development version is only expected to build with one GHC. When upgrading to GHC 9.14, CI would need to be updated as well.

If you want to support more than one GHC version, the considerations of #2379 are relevant.

[AlecsFerra]

-{-@ reflect id @-}
-{-@ reflect $ @-}
+{-@ assume reflect id as myId @-}
+
+{-@ reflect myId @-}
+myId :: a -> a
+myId x = x

We had pretty much the same issue a few versions ago. It turned out they added a new benchmarking function and ended up using it in the definition of id. To see if that’s what’s going on again, we should dump the Core, find the function name, and then assert in the Prelude that it’s equal to id

[AlecsFerra]

GHC 9.14.1:

makeId :: Ty -> Ctx -> Env -> Value
makeId = \ (σ_a1fV :: Ty) _ _ -> VFun σ_a1fV σ_a1fV breakpoint

GHC 9.12.2:

makeId :: Ty -> Ctx -> Env -> Value
makeId = \ (σ_a1cD :: Ty) _ _ -> VFun σ_a1cD σ_a1cD id

I think its the breakpoint thingy, it should be reflected as the identity function

[facundominguez]

I rebased develop, and contributed some commits.

I think its the breakpoint thingy, it should be reflected as the identity function

Might work. It is a change that can be separated from the upgrade, though. I think I would prefer to assume-reflect it most of the time, to verify with a simpler definition of id.

[AlecsFerra]

I rebased develop, and contributed some commits.

I think its the breakpoint thingy, it should be reflected as the identity function

Might work. It is a change that can be separated from the upgrade, though. I think I would prefer to assume-reflect it most of the time, to verify with a simpler definition of id.

I don't think we should break user code, we should be the ones providing that assume reflect

[facundominguez]

I don't think we should break user code, we should be the ones providing that assume reflect

👍 Feel free to make a pull request.

[facundominguez]

Thanks @gergoerdi again for submitting the fixes, and thanks @TeofilC for providing the patches in head.hackage that helped me testing earlier versions of the upgrade [link].