ucsd-progsys / liquidhaskell

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

Liquid Haskell crashes on higher-kinded polymorphism #2189

Open facundominguez opened 1 year ago

facundominguez commented 1 year ago

The composition from Control.Category makes Liquid Haskell crash. Here's an example

import qualified Control.Category

-- (Control.Category..) :: Category cat => (cat b c) -> (cat a b) -> cat a c
g :: a -> a
g = id Control.Category.. id

main :: IO ()
main = return ()

Verifying this file yields

$ liquidhaskell_boot_datadir=$PWD/liquidhaskell-boot cabal exec -- liquidhaskell test.hs
[1 of 1] Compiling Main             ( test.hs, test.o )

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

test.hs:4:1: error:
    • Uh oh.
    addC: malformed constraint:
cconsE: 
 t = lq_tmp$x##225:{VV : a | $k_##227[VV##226:=VV]} -> {VV : a | $k_##229[VV##228:=VV]}
 te = ('GHC.Types.BoxedRep 'GHC.Types.Lifted) -> {lq_tmp$x##295 : a | $k_##294[VV##293:=lq_tmp$x##295][lq_tmp$x##8:=lq_anf$##7205759403792800940##d1Uo][lq_tmp$x##9:=lq_anf$##7205759403792800941##d1Up]} {lq_tmp$x##292 : a | $k_##291[VV##290:=lq_tmp$x##292][lq_tmp$x##8:=lq_anf$##7205759403792800940##d1Uo][lq_tmp$x##9:=lq_anf$##7205759403792800941##d1Up]}Control.Category..
  @Type
  @(->)
  Control.Category.$fCategoryTYPEFUN
  @a
  @a
  @a
  lq_anf$##7205759403792800940
  lq_anf$##7205759403792800941('GHC.Types.BoxedRep 'GHC.Types.Lifted) -> {lq_tmp$x##295 : a | $k_##294[VV##293:=lq_tmp$x##295][lq_tmp$x##8:=lq_anf$##7205759403792800940##d1Uo][lq_tmp$x##9:=lq_anf$##7205759403792800941##d1Up]} {lq_tmp$x##292 : a | $k_##291[VV##290:=lq_tmp$x##292][lq_tmp$x##8:=lq_anf$##7205759403792800940##d1Uo][lq_tmp$x##9:=lq_anf$##7205759403792800941##d1Up]}
 <: 
lq_tmp$x##225:{VV : a | $k_##227[VV##226:=VV]} -> {VV : a | $k_##229[VV##228:=VV]}
    • 
  |
4 | g = id Control.Category.. id
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
ranjitjhala commented 1 year ago

Eeks, I wonder if this is some new un-handled construct in Core ?

facundominguez commented 1 year ago

This is not the first time that the composition from Control.Category gives trouble. There was at least #734.