Surprising(?) solving failure

[bgamari]

I was surprised to find that this program fails to typecheck with Thoralf:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fplugin=ThoralfPlugin.Plugin #-}

module ThisIsOnlyATest where

import GHC.TypeLits
import Data.Type.Bool
import Data.Proxy

type family Max (x :: Nat) (y :: Nat) :: Nat where
  Max n n = n
  Max x y = If (x <=? y) y x

g :: forall n. (1 <= n) => Proxy n -> ()
g = f

f :: forall n. (Max n 1 ~ n) => Proxy n -> ()
f Proxy = ()

Essentially, I am asking Thoralf to conclude that Max n 1 ~ n given that 1 <= n.

Thoralf appears to produce the following SMT script,

[send->] (push 1 )
[<-recv] success
[send->] (declare-const a2KY Int)
[<-recv] success
[send->] (declare-const a2Le Bool)
[<-recv] success
[send->] (assert (< 0 a2KY))
[<-recv] success
[send->] (assert (= (or (< 1 a2KY)  (= 1 a2KY)) a2Le ) )
[<-recv] success
[send->] (assert (= a2Le true ) )
[<-recv] success
[send->] (check-sat )
[<-recv] sat
[send->] (assert false )
[<-recv] success
[send->] (check-sat )
[<-recv] unsat
[send->] (pop 1 )
[<-recv] success
[send->] (exit )

This is a bit odd: everything up to the first (check-sat) looks fine (and indeed Z3 claims that the predicate, 0 < a2KY && (1 <= a2KY) == a2Le && a2Le == true, is satisfiable).

However, then Thoralf for some reason adds (assert false), which of course renders the whole thing unsatisfiable. I haven't dived too deep into the implementation, but this seems suspicious.

[bgamari]

Looking at the talk again, I think I see the rationale for the second (check-sat): we first assert that the givens are consistent and then assert that at least one wanted is false. However, in this case the wanted list appears to be empty:

Solver call start


	Givens: 
[
(<=? [1,n;a2KY:s],fsk;a2Le:t)
(fsk;a2Le:t,True [])
]
	Wanteds: 
[

]
	Desireds: 
[
(Max [n;a2KY:s,1],n;a2KY:s)
]

Decs:[
Atom "(declare-const a2KY Int)"
Atom "(declare-const a2Le Bool)"
Atom "(assert (< 0 a2KY))"
]

Givens :[
(List [Atom "=",Atom "(or (< 1 a2KY)  (= 1 a2KY))",Atom "a2Le"],(<=? [1,n;a2KY:s],fsk;a2Le:t))
(List [Atom "=",Atom "a2Le",Atom "true"],(fsk;a2Le:t,True []))
]

Wanteds :[

]

[goldfirere]

The problem might be the definition of Max. GHC can't reduce Max n 1 to anything Thoralf knows about, so it doesn't have any wanteds to try to solve. Perhaps trying removing the first equation of Max?

[bgamari]

Removing the first equation results in,

src/Hi.hs:21:5: error:
    • Could not deduce: If (n <=? 1) 1 n ~ n arising from a use of ‘f’
      from the context: 1 <= n
        bound by the type signature for:
                   g :: forall (n :: Nat). (1 <= n) => Proxy n -> ()
        at src/Hi.hs:20:1-40
      ‘n’ is a rigid type variable bound by
        the type signature for:
          g :: forall (n :: Nat). (1 <= n) => Proxy n -> ()
        at src/Hi.hs:20:1-40
    • In the expression: f
      In an equation for ‘g’: g = f
    • Relevant bindings include
        g :: Proxy n -> () (bound at src/Hi.hs:21:1)

[goldfirere]

Perhaps Thoralf was never taught about If. @Divesh-Otwani ?

[bgamari]

Indeed Thoralf was ignorant of If. This is fixed in #7.

There are a variety of preparatory patches which clean up various things on the way.