Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR provides a temporary fix for issue #2535 by addressing a bug that caused an invariant violation and adjusting type matching in LiquidHaskell. Key changes include:
- Adding a new test in tests/pos/T2535.hs to reproduce the issue.
- Removing the guard in the RApp case in Plugged.hs to allow processing of type arguments with potentially different lengths.
- Modifying the isKind function in Misc.hs to work around a bug in GHC-9.12.2 by hardcoding a condition on "GHC.Types.Type".
Reviewed Changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| tests/pos/T2535.hs | Introduces a test case dealing with AB values and the check measure. |
| liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Plugged.hs | Removes the length equality check, which might affect the alignment of type arguments. |
| liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Misc.hs | Updates the isKind function with a temporary hack addressing a known GHC bug. |
| {-@ g :: {v:AB a | check v} -> {v:AB a | check v} @-} | ||
| g :: forall a. AB a -> AB a | ||
| g (A x) = A x | ||
| g (B x) = B x No newline at end of file |
There was a problem hiding this comment.
The pattern match for 'B' in function 'g' returns a value that does not satisfy the 'check' measure as required by the type signature, potentially violating the intended invariant. Consider revisiting the definition of 'g' or adjusting the 'check' measure to ensure consistency.
| g (B x) = B x | |
| g (B x) = error "Invalid input: B does not satisfy the check measure" |
|
|
||
| isKind k = isTYPEorCONSTRAINT k -- TODO:GHC-863 isStarKind k -- typeKind k | ||
| || case k of | ||
| TyVarTy kk -> (showPpr (varType kk)) == "GHC.Types.Type" |
There was a problem hiding this comment.
Hardcoding the string 'GHC.Types.Type' for the type check is fragile and may break with future changes; consider adding robust documentation or a more resilient condition to clarify this temporary workaround.
| TyVarTy kk -> (showPpr (varType kk)) == "GHC.Types.Type" | |
| TyVarTy kk -> varType kk == typeKind (mkTyConTy typeTyCon) |
|
|
||
| isKind k = isTYPEorCONSTRAINT k -- TODO:GHC-863 isStarKind k -- typeKind k | ||
| || case k of | ||
| TyVarTy kk -> showPpr (varType kk) == ghcTypeStr |
There was a problem hiding this comment.
It would be better not to hardcode the string, as GHC sometimes moves definitions and the string changes, requiring debugging to catch it.
varType kk == GHC.Builtin.Types.liftedTypeKind would be cheaper to maintain.
facundominguez
left a comment
There was a problem hiding this comment.
👋 Hello Niki! The PR looks good to me, though I share some requests to make the code easier to maintain.
Also, I think you will want to list tests/pos/T2535.hs in tests.cabal or it won't be tested when running tests.
| throwError (err (F.pprint hsT) (F.pprint lqT)) | ||
|
|
||
| -- Niki believes there is a bug on the isTYPEorCONSTRAINT function in GHC-9.12.2 | ||
| -- Hardcoding "GHC.Types.Type" for now because typeKind in in the Prim module... |
There was a problem hiding this comment.
Is there an issue reported in GHC? Otherwise, what is the problem referred here?
| throwError (err (F.pprint hsT) (F.pprint lqT)) | ||
|
|
||
| -- Niki believes there is a bug on the isTYPEorCONSTRAINT function in GHC-9.12.2 | ||
| -- Hardcoding "GHC.Types.Type" for now because typeKind in in the Prim module... |
There was a problem hiding this comment.
I don't understand the comment about typeKind being in some module Prim, but there is a function GHC.Core.Type.typeKind.
The goal is to fix #2535 but it seems it trigered another bug.
Concretely, for the type:
The function isKind k, was returning false.
The fix is temporal, since I believe the isTYPEorCONSTRAINT function in GHC-9.12.2 is wrong...