[bug] crash related to Control.Arrow.first

[plredmond]

Problem: The following snippet of code causes a crash in LH.

import Control.Arrow (first)
{-@ crash :: {x:_ | x == True } @-}
crash :: Bool
crash = const True (first id)

Expected: LH should ignore the second argument to const and accept the snippet. Actual: The second argument to const being variations on use of the typeclass method first all cause a crash within LH:

• first id
• first id ((),())
• first id (True, True)

Crash output:

**** LIQUID: ERROR :1:1-1:1: Error
  elaborate solver elabBE 89 "lq_anf$##7205759403792814479##d5qL" {lq_tmp$x##440 : func(0 , [(Tuple (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)));
                           (Tuple (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)))]) | [(lq_tmp$x##440 = (Control.Arrow.first lq_anf$##7205759403792814478##d5qK));
                                                                                                                                                (lq_tmp$x##440 = (Control.Arrow.first lq_anf$##7205759403792814478##d5qK))]} failed on:
      (lq_tmp$x##440 == Control.Arrow.first lq_anf$##7205759403792814478##d5qK
       && lq_tmp$x##440 == Control.Arrow.first lq_anf$##7205759403792814478##d5qK)
  with error
      Cannot unify (@(45) @(42) @(43)) with func(0 , [(GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep));
          (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep))]) in expression: Control.Arrow.first lq_anf$##7205759403792814478##d5qK
  in environment
      Control.Arrow.first := func(4 , [(@(3) @(0) @(1));
                                       (@(3) (Tuple @(0) @(2)) (Tuple @(1) @(2)))])

      lq_anf$##7205759403792814478##d5qK := func(0 , [(GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep));
                                                      (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep))])

      lq_tmp$x##440 := func(0 , [(Tuple (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)));
                                 (Tuple (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)) (GHC.Types.Any (GHC.Prim.TYPE GHC.Types.LiftedRep)))])

Version: Crash occurs on

• build-from-source https://github.com/ucsd-progsys/liquidhaskell/commit/ad7f0cf5b86cb62fa855f3392bfa34f65225c4ed
• hackage package versions liquid-base-4.14.1.0,liquid-prelude-0.8.10.2,liquidhaskell-0.8.10.2

[plredmond]

I've tried other variations (such as, eg. length, which is also typeclass method) but wasn't able to reproduce the crash

[kosmikus]

I cannot reproduce this with released liquidhaskell-0.8.10.2, liquid-base-4.14.1.0. I don't think liquid-prelude is needed here. I'll try with the specified commit.

[kosmikus]

I cannot reproduce this with the given commit either. The file yields SAFE (2 constraints checked) for me.

[plredmond]

I'm building with nix, using a recent nixos-20.03 package set with some overrides:

• built-from-source https://github.com/plredmond/liquidhaskell/blob/nixify/default.nix
• built-from-hackage https://github.com/plredmond/liquidhaskell/blob/nixify-hackage/default.nix

It's possible that the crash I've found is related to an old version of some haskell dependency in the nixos-20.03 package set which I'm not overriding.

When nixos-20.09 is stable (and the whole package set is updated) I'll update this bug. It's likely that the bug will be resolved.

[plredmond]

These are the build flags I'm using:

-fplugin=LiquidHaskell
-fplugin-opt=LiquidHaskell:--exact-data
-fplugin-opt=LiquidHaskell:--reflection
-fplugin-opt=LiquidHaskell:--ple
-fplugin-opt=LiquidHaskell:--no-adt
-Wall
-threaded
-rtsopts
-with-rtsopts=-N

[kosmikus]

Ok, that helps. I can now reproduce the crash both with the released version and with current develop:

{-@ LIQUID "--reflection" @-}
module Bug where

import Control.Arrow (first)

{-@ crash :: {x:_ | x == True } @-}
crash :: Bool
crash = const True (first id)

[plredmond]

I haven't kept the habit of adding these feature flags to my source-code, and instead put them all in the project config file. I'm glad you thought to ask!

[adinapoli]

Interestingly enough, using first from Data.Bifunctor works just fine using one of those "fully instantiated" examples that @plredmond posted:

{-@ LIQUID "--reflection" @-}
module T1772 where

import Data.Bifunctor (first)

{-@ crash :: {x:_ | x == True } @-}
crash :: Bool
crash = const True (first id ((),()))

At first (no pun intended!) I would have said the culprit was the fact that first id (without extra arguments) has type (b, d) -> (b, d) and somehow LH is not able to deal with it, but it's strange that the snippet I just posted would not work with Control.Arrow.first but would work just fine with Data.Bifunctor.