ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 135 forks source link

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

Open amigalemming opened 6 months ago

amigalemming commented 6 months ago

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 commented 4 months ago

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

nikivazou commented 4 months ago

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.