Awful error message due to unsorted refinement

[gridaphobe]

module Blank where

data Graph = Node Int [Graph]

{-@ 
measure glen :: Graph -> Int
glen (Node i gs) = 1 + glens gs
@-}
{-@ invariant {v: Graph | glen v >= 0} @-}

{-@ 
measure glens :: [Graph] -> Int
glens [] = 0
glens (g:gs) = glen g + glens gs
@-}
{-@ invariant {v: [Graph] | glens v >= 0} @-}

{-@ extract :: [Int] -> g:Graph -> Graph / [glen g] @-}
extract :: [Int] -> Graph -> Graph
extract ps (Node x xs) = if x `elem` ps
    then Node x []
    else Node x (map (extract (x:ps)) xs)

$ liquid Blank.hs
...
:1:1-1:1: Error
  elaborate solver elabBE 25 "lq_anf$##1677725092##dUk" {lq_tmp$x##211 : [int] | [((glens lq_tmp$x##211) = ((glen x##alI) + (glens ps##alH)));
                          ((len lq_tmp$x##211) = (1 + (len ps##alH)));
                          ((null lq_tmp$x##211) <=> false);
                          ((tail lq_tmp$x##211) = ps##alH);
                          ((head lq_tmp$x##211) = x##alI);
                          ((len lq_tmp$x##211) >= 0)]} failed on:
      (((((glens lq_tmp$x##211 == glen x##alI + glens ps##alH
           && len lq_tmp$x##211 == 1 + len ps##alH)
          && (null lq_tmp$x##211 <=> false))
         && tail lq_tmp$x##211 == ps##alH)
        && head lq_tmp$x##211 == x##alI)
       && len lq_tmp$x##211 >= 0)
  with error
      The sort Blank.Graph is not numeric
  because
Cannot unify Blank.Graph with int in expression: glens lq_tmp$x##211
  in environment
      ps##alH := [int]

      tail := func(1, [[@(0)]; [@(0)]])

      glen := func(0, [Blank.Graph; int])

      glens := func(0, [[Blank.Graph]; int])

      len := func(2, [(@(0)  @(1)); int])

      x##alI := int

      null := func(1, [[@(0)]; bool])

      lq_tmp$x##211 := [int]

      head := func(1, [[@(0)]; @(0)])

The error goes away if you add --prune-unsorted

[alanz]

FYI here is another example, which has the same problem. On 0.7, not 0.6 The problem goes away with --prune-unsorted.

{-@ measure size @-}
{-@ size :: xs:[a] -> {v:Nat | v = size xs} @-}
size :: [a] -> Int
size [] = 0
size (_:rs) = 1 + size rs

{-@ measure subsize @-}
{-@ subsize :: xs:[[a]] -> {v:Nat | v == subsize xs} @-}
subsize :: [[a]] -> Int
subsize [] = 0
subsise (x:_) = size x

It gives

:1:1-1:1: Error
  elaborate solver elabBE 17 "ds_dwe" {VV##199 : [a_amW] | [((subsize VV##199) >= 0);
                      ((len VV##199) >= 0);
                      (((len VV##199) < (len ds_dwe)) => && [((size VV##199) >= 0)])]} failed on:
      ((subsize VV##199 >= 0
        && len VV##199 >= 0)
       && (len VV##199 < len ds_dwe => size VV##199 >= 0))
  with error
      Cannot unify [@(42)] with a_amW in expression: subsize VV##199
  in environment
      subsize := func(1, [[[@(0)]]; int])

      size := func(1, [[@(0)]; int])

      ds_dwe := [a_amW]

      len := func(2, [(@(0)  @(1)); int])

      VV##199 := [a_amW]

[ranjitjhala]

Yikes ok this is horrible. Let me put this next on my plate...

On Mon, Mar 6, 2017 at 12:13 PM Alan Zimmerman notifications@github.com wrote:

FYI here is another example, which has the same problem. On 0.7, not 0.6 The problem goes away with --prune-unsorted.

{-@ measure size @-} {-@ size :: xs:[a] -> {v:Nat | v = size xs} @-}size :: [a] -> Int size [] = 0 size (_:rs) = 1 + size rs

{-@ measure subsize @-} {-@ subsize :: xs:[[a]] -> {v:Nat | v == subsize xs} @-} subsize :: [[a]] -> Int subsize [] = 0 subsise (x:_) = size x

It gives

:1:1-1:1: Error elaborate solver elabBE 17 "ds_dwe" {VV##199 : [a_amW] | [((subsize VV##199) >= 0); ((len VV##199) >= 0); (((len VV##199) < (len ds_dwe)) => && [((size VV##199) >= 0)])]} failed on: ((subsize VV##199 >= 0 && len VV##199 >= 0) && (len VV##199 < len ds_dwe => size VV##199 >= 0)) with error Cannot unify [@(42)] with a_amW in expression: subsize VV##199 in environment subsize := func(1, [[[@(0)]]; int])

  size := func(1, [[@(0)]; int])

  ds_dwe := [a_amW]

  len := func(2, [(@(0)  @(1)); int])

  VV##199 := [a_amW]

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/934#issuecomment-284315261, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOP8GzyboeyjwPGqQt09vFwxzcyqVks5ri6sVgaJpZM4LxrS8 .

[alanz]

And I just noticed a typo in my example, the last equation name is subsise instead of subsize. It does not affect the error though.

[RyanGlScott]

I also ran into this issue recently. In case you want more test cases, here is the complete program which trips up this bug:

{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--totality"           @-}
{-@ LIQUID "--exactdc" @-}
{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE FlexibleInstances, IncoherentInstances, MultiParamTypeClasses, TypeFamilies #-}
module Bug where

import Prelude hiding (Either(..))
import GHC.Generics

infixl 3 ==., ?
infixl 2 ***

type Proof = ()

(?) :: (Proof -> a) -> Proof -> a
f ? y = f y

data QED = QED

(***) :: a -> QED -> Proof
_ *** _ = ()

class OptEq a r where
  (==.) :: a -> a -> r

instance (a~b) => OptEq a (Proof -> b) where
{- instance OptEq a (Proof -> b) where
  ==. :: x:a -> y:a -> {v:Proof | x == y} -> {v:b | v ~~ x && v ~~ y}
  -}
  (==.) x _ _ = x

instance (a~b) => OptEq a b where
{- instance OptEq a b where
  ==. :: x:a -> y:{a| x == y} -> {v:b | v ~~ x && v ~~ y }
  -}
  (==.) x _ = x

{-@ data (:+:) f g p = L1 (f p) | R1 (g p) @-}
type Sum = (:+:)

{-@ data (:*:) f g p = (:*:) (f g) (g p) @-}
type Prod = (:*:)

{-@ axiomatize eqProd @-}
eqProd :: (f p -> f p -> Bool) -> (g p -> g p -> Bool)
       -> (f :*: g) p -> (f :*: g) p -> Bool
eqProd eqFp eqGp (p1 :*: p2) (q1 :*: q2) = eqFp p1 q1 && eqGp p2 q2

{-@ eqProdRefl :: eqFp:(f p -> f p -> Bool) -> eqFpRefl:(x:f p -> { eqFp x x })
               -> eqGp:(g p -> g p -> Bool) -> eqGpRefl:(y:g p -> { eqGp y y })
               -> p:Prod f g p
               -> { eqProd eqFp eqGp p p }
@-}
eqProdRefl :: (f p -> f p -> Bool) -> (f p -> Proof)
           -> (g p -> g p -> Bool) -> (g p -> Proof)
           -> (f :*: g) p -> Proof
eqProdRefl eqFp eqFpRefl eqGp eqGpRefl p@(x :*: y) =
      eqProd eqFp eqGp p p
  ==. (eqFp x x && eqGp y y)
  ==. (True && eqGp y y) ? eqFpRefl x
  ==. (True && True)     ? eqGpRefl y
  ==. True
  *** QED

LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************          

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

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

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  elaborate solver elabBE 98 "lq_anf$##1677726315##d1e3" {lq_tmp$x##674 : (GHC.Generics.$58$$42$$58$  f_a1bC  g_a1bE  p_a1bD) | [(lq_tmp$x##674 = p##a1ak);
                                                                        ((lq_tmp$db##1 lq_tmp$x##674) = y##a1am);
                                                                        ((lq_tmp$db##0 lq_tmp$x##674) = x##a1al);
                                                                        ((select_$58$$42$$58$_2 lq_tmp$x##674) = y##a1am);
                                                                        ((select_$58$$42$$58$_1 lq_tmp$x##674) = x##a1al);
                                                                        ((is_$58$$42$$58$ lq_tmp$x##674) <=> true);
                                                                        ((lq_tmp$db##1 lq_tmp$x##674) = y##a1am);
                                                                        ((lq_tmp$db##0 lq_tmp$x##674) = x##a1al);
                                                                        ((select_$58$$42$$58$_2 lq_tmp$x##674) = y##a1am);
                                                                        ((select_$58$$42$$58$_1 lq_tmp$x##674) = x##a1al);
                                                                        ((is_$58$$42$$58$ lq_tmp$x##674) <=> true)]} failed on:
      ((lq_tmp$x##674 == p##a1ak
        && ((((lq_tmp$db##1 lq_tmp$x##674 == y##a1am
               && lq_tmp$db##0 lq_tmp$x##674 == x##a1al)
              && select_:*:_2 lq_tmp$x##674 == y##a1am)
             && select_:*:_1 lq_tmp$x##674 == x##a1al)
            && (is_:*: lq_tmp$x##674 <=> true)))
       && ((((lq_tmp$db##1 lq_tmp$x##674 == y##a1am
              && lq_tmp$db##0 lq_tmp$x##674 == x##a1al)
             && select_:*:_2 lq_tmp$x##674 == y##a1am)
            && select_:*:_1 lq_tmp$x##674 == x##a1al)
           && (is_:*: lq_tmp$x##674 <=> true)))
  with error
      Cannot unify GHC.Generics.$58$$43$$58$ with GHC.Generics.$58$$42$$58$ in expression: lq_tmp$db##1 lq_tmp$x##674
  in environment
      select_:*:_1 := func(3, [(GHC.Generics.$58$$42$$58$  @(0)  @(1)  @(2));
                               (@(0)  @(2))])

      lq_tmp$db##0 := func(3, [(GHC.Generics.$58$$43$$58$  @(0)  @(1)  @(2));
                               (@(0)  @(2))])

      lq_tmp$db##1 := func(3, [(GHC.Generics.$58$$43$$58$  @(0)  @(1)  @(2));
                               (@(1)  @(2))])

      is_:*: := func(3, [(GHC.Generics.$58$$42$$58$  @(0)  @(1)  @(2));
                         bool])

      p##a1ak := (GHC.Generics.$58$$42$$58$  f_a1bC  g_a1bE  p_a1bD)

      select_:*:_2 := func(3, [(GHC.Generics.$58$$42$$58$  @(0)  @(1)  @(2));
                               (@(1)  @(2))])

      x##a1al := (f_a1bC  p_a1bD)

      lq_tmp$x##674 := (GHC.Generics.$58$$42$$58$  f_a1bC  g_a1bE  p_a1bD)

      y##a1am := (g_a1bE  p_a1bD)

Adding --prune-unsorted fixes the issue, as expected.

I'm on commit 904e6927a97480856fe2c7d2e083f7bc7a0710c5, FWIW.