crash: SMTLIB2 with desugared typeclass

[yiyunliu]

I don't know how I can reduce it further, but the following desugared type class causes SMTLIB crash with the error message: :1:1-1:1: Error crash: SMTLIB2 respSat = Error "line 327 column 1992: Sorts (Subclass2.MyFunctor Int) and (Subclass2.MyFunctor (Subclass2.MyId Int)) are incompatible"

{-# LANGUAGE RankNTypes #-}
{-@ LIQUID "--reflection" @-}
module Subclass2 where

data MyFunctor f = CMyFunctor {myfmap :: forall a b. (a -> b) -> f a -> f b}

{-@ reflect myid @-}
myid :: a -> a
myid x = x

{-@ data MyApplicative f = CMyApplicative
  { p1MyApplicative :: MyFunctor f
  , myprop :: forall a b. x:f a -> f:(a -> b) -> {myid x /= x}
  } @-}

data MyApplicative f = CMyApplicative
  { p1MyApplicative :: MyFunctor f
  , myprop :: forall a b.f a -> (a -> b) -> ()
  }

data MyId a = MyId a

fMyFunctorMyId :: MyFunctor MyId
fMyFunctorMyId = CMyFunctor (\f (MyId x) -> MyId (f x))

cmyprop :: MyId a -> (a -> b) -> ()
cmyprop _ _ = ()

fMyApplicativeMyId :: MyApplicative MyId
fMyApplicativeMyId = CMyApplicative fMyFunctorMyId cmyprop

When replacing fMyFunctorMyId by its definition in fMyApplicativeMyId, the issue goes away and liquid correctly returns unsafe.

[ranjitjhala]

This typically means that a malformed (Ill types) refinement is getting generated somewhere.

Is this on develop?

You can look at the .smt file to see where.

I think the first thing is to add support to Fixpoint so that instead of Crashing it points to the constraint and hence, Haskell source that tickles the problem.

On Fri, Feb 14, 2020 at 7:58 AM Yiyun Liu notifications@github.com wrote:

I don't know how I can reduce it further, but the following desugared type class causes SMTLIB crash with the error message: :1:1-1:1: Error crash: SMTLIB2 respSat = Error "line 327 column 1992: Sorts (Subclass2.MyFunctor Int) and (Subclass2.MyFunctor (Subclass2.MyId Int)) are incompatible"

{-# LANGUAGE RankNTypes #-} {-@ LIQUID "--reflection" @-}module Subclass2 where data MyFunctor f = CMyFunctor {myfmap :: forall a b. (a -> b) -> f a -> f b}

{-@ reflect myid @-}myid :: a -> a myid x = x

{-@ data MyApplicative f = CMyApplicative { p1MyApplicative :: MyFunctor f , myprop :: forall a b. x:f a -> f:(a -> b) -> {myid x /= x} } @-} data MyApplicative f = CMyApplicative { p1MyApplicative :: MyFunctor f , myprop :: forall a b.f a -> (a -> b) -> () } data MyId a = MyId a fMyFunctorMyId :: MyFunctor MyId fMyFunctorMyId = CMyFunctor (\f (MyId x) -> MyId (f x)) cmyprop :: MyId a -> (a -> b) -> () cmyprop = () fMyApplicativeMyId :: MyApplicative MyId fMyApplicativeMyId = CMyApplicative fMyFunctorMyId cmyprop

When replacing fMyFunctorMyId by its definition in fMyApplicativeMyId, the issue goes away and liquid correctly returns unsafe.

— 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/1613?email_source=notifications&email_token=AAMS4OBI5LK5WL4VTMPAAGDRC25RTA5CNFSM4KVK2HKKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4INTQ6EA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4ODTXIKB3LS7YK7PJZLRC25RTANCNFSM4KVK2HKA .

[nikivazou]

I am on it!

[yiyunliu]

@nikivazou Not sure if it's anyhow related, but changing data MyId to newtype MyId causes the full version of the desugared example to give the following error message:

/home/alsymd/git/liquidhaskell-debug/Subclass2.hs:56:68-56:75: Error
  elaborate solver failed on:
      Subclass2.cmyap (Subclass2.cmypure lq_tmp$x##729) lq_tmp$x##728 == Subclass2.myfmap Subclass2.cp1MyApplicative lq_tmp$x##729 lq_tmp$x##728
  with error
      Cannot unify a##a1qf with (a##asg a##a1qf) in expression: Subclass2.myfmap Subclass2.cp1MyApplicative lq_tmp$x##729 lq_tmp$x##728 << ceq2 >>
  in environment
      Subclass2.cmyap := func(2 , [func(0 , [@(0); @(1)]); @(0); @(1)])

      Subclass2.cmypure := func(1 , [@(0); @(0)])

      Subclass2.cp1MyApplicative := (Subclass2.MyFunctor a##asg)

      Subclass2.myfmap := func(3 , [(Subclass2.MyFunctor @(0));
                                    func(0 , [@(1); @(2)]);
                                    (@(0) @(1));
                                    (@(0) @(2))])

      lq_tmp$x##728 := a##a1qf

      lq_tmp$x##729 := func(0 , [a##a1qf; b##a1qg])

Here's the full program:

{-# LANGUAGE RankNTypes #-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
module Subclass2 where

{-@ data MyFunctor f = CMyFunctor {myfmap :: forall a b. (a -> b) -> f a -> f b} @-}
data MyFunctor f = CMyFunctor {myfmap :: forall a b. (a -> b) -> f a -> f b}

{-@ reflect myid @-}
myid :: a -> a
myid x = x

{-@ data MyApplicative f = CMyApplicative
  { p1MyApplicative :: MyFunctor f
  , mypure :: forall a. a -> f a
  , myap :: forall a b. f (a -> b) -> f a -> f b
  , myprop :: forall a b. x:f a -> f:(a -> b) -> {myap (mypure f) x == myfmap p1MyApplicative f x}
  } @-}

data MyApplicative f = CMyApplicative
  { p1MyApplicative :: MyFunctor f
  , mypure :: forall a. a -> f a
  , myap :: forall a b.f (a -> b) -> f a -> f b
  , myprop :: forall a b.f a -> (a -> b) -> ()
  }

newtype MyId a = MyId a

{-@ reflect cmyfmap @-}
cmyfmap :: (a -> b) -> MyId a -> MyId b
cmyfmap f (MyId a) = MyId (f a)

{-@ reflect fMyFunctorMyId @-}
fMyFunctorMyId :: MyFunctor MyId
fMyFunctorMyId = CMyFunctor cmyfmap

{-@ reflect cp1MyApplicative @-}
cp1MyApplicative :: MyFunctor MyId
cp1MyApplicative = fMyFunctorMyId

{-@ reflect cmypure @-}
cmypure :: a -> MyId a
cmypure = MyId

{-@ reflect cmyap @-}
cmyap :: MyId (a -> b) -> MyId a -> MyId b
cmyap (MyId f) (MyId a) = MyId (f a)

{-@ reflect cmyprop @-}
cmyprop :: MyId a -> (a -> b) -> ()
cmyprop _ _ = ()

{-@ reflect fMyApplicativeMyId @-}
fMyApplicativeMyId :: MyApplicative MyId
fMyApplicativeMyId = CMyApplicative cp1MyApplicative cmypure cmyap cmyprop

[nikivazou]

Oh, no... This is related to my newtype edit... I replaced newtypes with their RHS too early...

For the newtype newtype tleft = T tright I told LH to totally replace tleft with tright before it goes in the logic. Now, there is x :: MyId a (which in the logic has just x :: a) and wants to be applied in a position that expected an a1 a2.

If it is blocking you, add the below two cases at the beginning of sort unification function (https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/SortCheck.hs#L1068) to ignore type unification in the presence of type application:

unify1 _ _ θ (FApp _ _) _ 
  = return θ
unify1 _ _ θ _ (FApp _ _)
  = return θ

I will soon provide a proper solution, but this will require keeping the newtypes around longer.

[yiyunliu]

No worries. We can use data for now and switch to newtype when it becomes available.