Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"addC: malformed constraint: cconsE" in closed-world class #2277

Open
amigalemming opened this issue Apr 3, 2024 · 2 comments
Open

"addC: malformed constraint: cconsE" in closed-world class #2277

amigalemming opened this issue Apr 3, 2024 · 2 comments

Comments

@amigalemming
Copy link

Consider this module:

module Data.Array.Comfort.Shape where

import Control.DeepSeq (NFData, rnf)


data Lower = Lower
data Upper = Upper

class TriangularPart part where
   switchTriangularPart :: f Lower -> f Upper -> f part
instance TriangularPart Lower where switchTriangularPart f _ = f
instance TriangularPart Upper where switchTriangularPart _ f = f

data Triangular part size =
   Triangular {
      triangularPart :: part,
      triangularSize :: size
   } deriving (Show)

newtype Flip f b a = Flip {getFlip :: f a b}

instance (TriangularPart part, NFData size) => NFData (Triangular part size) where
   rnf (Triangular part sz) =
      rnf
         (flip getFlip part $
            switchTriangularPart (Flip $ \Lower -> ()) (Flip $ \Upper -> ()),
          sz)

LiquidHaskell/GHC-9.6.3 complains:

src/Data/Array/Comfort/Shape.hs:26:11: error:
    Uh oh.
    addC: malformed constraint:
cconsE: 
 t = lq_tmp$x##1052:{lq_tmp$x##1083 : (Data.Array.Comfort.Shape.Flip {lq_tmp$x##1080 : (GHC.Prim.FUN {lq_tmp$x
...
   |
26 |          (flip getFlip part $
   |           ^^^^^^^^^^^^^^^^^

This is a simplified version of:
https://hackage.haskell.org/package/comfort-array-0.5.4.2/docs/Data-Array-Comfort-Shape.html

@facundominguez
Copy link
Collaborator

First stop: figuring out what the error message means 🙈
I'm attaching the full error output.

@nikivazou
Copy link
Member

It comes from here: https://github.com/ucsd-progsys/liquidhaskell/blob/develop/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs#L360

LH is adding a subtype constraint with the two huge types that are printed in the error and checks that these two types have the same Haskell type. This error message says that they do not have the same Haskell type.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants