Haskell cannot infer the type (or type-level Nat) equalities despite being explicitly annotated?

Question

I was trying to implement a Braun Tree with Haskell, defined like this:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}

data BraunTree (n :: Nat) a where
    Empty :: BraunTree 0 a
    Fork :: a -> BraunTree n a -> 
            BraunTree m a ->
            Either (n :~: m) (n :~: (m + 1)) ->
            BraunTree (n + m + 1) a

Now, I am trying to experiment with how I can "typesafely" insert things into this tree.

insert :: a -> BraunTree (n :: Nat) a -> BraunTree (n + 1 :: Nat) a
insert x Empty = Fork x Empty Empty (Left Refl)
insert x (Fork y (t1 :: BraunTree p a) (t2 :: BraunTree q a) (Left (Refl :: p :~: q))) = Fork x (t1' :: BraunTree (p + 1) a) (t2 :: BraunTree q a) (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
    where
        t1' :: BraunTree (p + 1) a
        t1' = insert x t1

with sucCong as

sucCong :: ((p :: Nat) :~: (q :: Nat)) -> (p + 1 :: Nat) :~: (q + 1 :: Nat)
sucCong Refl = Refl

Now, while the first clause of the insert compiles fine, the second line throws a confusing error.

/home/agnishom/test/typeExp/braun.hs:31:90: error:
    • Could not deduce: (((n1 + 1) + n1) + 1) ~ (n + 1)
      from the context: n ~ ((n1 + m) + 1)
        bound by a pattern with constructor:
                   Fork :: forall a (n :: Nat) (m :: Nat).
                           a
                           -> BraunTree n a
                           -> BraunTree m a
                           -> Either (n :~: m) (n :~: (m + 1))
                           -> BraunTree ((n + m) + 1) a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:11-85
      or from: m ~ n1
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘insert’
        at /home/agnishom/test/typeExp/braun.hs:31:69-72
      Expected type: BraunTree (n + 1) a
        Actual type: BraunTree (((n1 + 1) + m) + 1) a
      NB: ‘+’ is a type function, and may not be injective
    • In the expression:
        Fork
          x
          (t1' :: BraunTree (p + 1) a)
          (t2 :: BraunTree q a)
          (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
      In an equation for ‘insert’:
          insert
            x
            (Fork y
                  (t1 :: BraunTree p a)
                  (t2 :: BraunTree q a)
                  (Left (Refl :: p :~: q)))
            = Fork
                x
                (t1' :: BraunTree (p + 1) a)
                (t2 :: BraunTree q a)
                (Right (sucCong Refl :: (p + 1) :~: (q + 1)))
            where
                t1' :: BraunTree (p + 1) a
                t1' = insert x (t1 :: BraunTree p a)
    • Relevant bindings include
        t1' :: BraunTree (n1 + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:34:9)
        t1 :: BraunTree n1 a
          (bound at /home/agnishom/test/typeExp/braun.hs:31:19)
        insert :: a -> BraunTree n a -> BraunTree (n + 1) a
          (bound at /home/agnishom/test/typeExp/braun.hs:29:1)

I am not sure what I am doing wrong here. Also, why does haskell think that t1 :: BraunTree n1 a (in the error message), even though I have annotated t1 :: BraunTree p a?

Help with interpreting this error message would be very helpful

Answer 1

You could try to use this compiler plugin which infers type equalities for Nats for you automatically:

• https://github.com/clash-lang/ghc-typelits-natnormalise

Answer 2

GHC does not know that addition is commutative and associative.

I get a slightly different error, after removing some type sigs. Here it's clear that all the same terms appear, but in a different order:

• Could not deduce: (((n1 + 1) + m) + 1) ~ (n + 1)
  from the context: n ~ ((n1 + m) + 1)

The original equation is equivalent, but inconsistently replaces m with n1.

Unfortunately, I'm not sure how to help GHC out if you stick with the built-in Nat. I'm pretty sure you can switch to your own Nat, and prove the necessary equality. I don't know if there is a suitable library of such theorems yet.

Answer 3

You have too many type signatures. It's very hard to read through them. Also, sucCong is not necessary. Let's just clean this up first:

insert :: a -> BraunTree n a -> BraunTree (n + 1) a
insert x Empty = Fork x Empty Empty (Left Refl)
insert x (Fork y t1 t2 (Left Refl)) = Fork x (insert x t1) t2 (Right Refl)
-- by matching on Refl       ^^^^ you already prove that p ~ q
-- and (p + 1) ~ (q + 1) just follows naturally (i.e. is Refl)       ^^^^
-- if you just bound the equality to a variable, then sucCong would be necessary
-- as it would match the variable to Refl "for" you.

The error is the same

Braun.hs:#:39: error:
    • Could not deduce: (((n1 + 1) + n1) + 1) ~ (n + 1)
      from the context: n ~ ((n1 + m) + 1)
        bound by a pattern with constructor:
                   Fork :: forall a (n :: Nat) (m :: Nat).
                           a
                           -> BraunTree n a
                           -> BraunTree m a
                           -> Either (n :~: m) (n :~: (m + 1))
                           -> BraunTree ((n + m) + 1) a,
                 in an equation for ‘insert’
        at Braun.hs:#:11-34
      or from: m ~ n1
        bound by a pattern with constructor:
                   Refl :: forall k (a :: k). a :~: a,
                 in an equation for ‘insert’
        at Braun.hs:#:30-33
      Expected type: BraunTree (n + 1) a
        Actual type: BraunTree (((n1 + 1) + m) + 1) a
      NB: ‘+’ is a non-injective type family
    • In the expression: Fork x (insert x t1) t2 (Right Refl)
      In an equation for ‘insert’:
          insert x (Fork y t1 t2 (Left Refl))
            = Fork x (insert x t1) t2 (Right Refl)
    • Relevant bindings include
        t1 :: BraunTree n1 a (bound at Braun.hs:#:18)
        insert :: a -> BraunTree n a -> BraunTree (n + 1) a
          (bound at Braun.hs:#:1)
  |
# | insert x (Fork y t1 t2 (Left Refl)) = Fork x (insert x t1) t2 (Right Refl)
  |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Per the bottom of the message, n1 is the index of t1, and you called it p. We also know that m (t2's index) is equal to p, and that n (the function argument) is equal to (p + m) + 1. Let's apply all the substitutions we can to the constraint that's failing:

(((n1 + 1) + n1) + 1) ~ (n + 1)
-- rename n1 to p
(((p + 1) + p) + 1) ~ (n + 1)
-- substitute n ~ (p + m) + 1
(((p + 1) + p) + 1) ~ (((p + m) + 1) + 1)
-- m ~ p
(((p + 1) + p) + 1) ~ (((p + p) + 1) + 1)

The issue is that GHC cannot prove that ((p + 1) + p) ~ ((p + p) + 1). If you had used a nicer Nat, one that wasn't built in to the compiler, it would be possible to prove that this is true yourself. As it is, the sanest idea is probably:

{-# LANGUAGE AllowAmbiguousTypes #-}
import Unsafe.Coerce
-- using TypeApplications usually means using AllowAmbiguousTypes

-- it is also possible to use a compiler plugin to "teach" GHC the laws
-- of arithmetic
-- by keeping the unsafeCoerce in these wrappers, you decrease the chance of
-- "proving" something that isn't actually true.
plusAssoc :: forall l m r. ((l + m) + r) :~: (l + (m + r))
plusAssoc = unsafeCoerce Refl
plusComm :: forall l r. (l + r) :~: (r + l)
plusComm = unsafeCoerce Refl

insert :: a -> BraunTree n a -> BraunTree (n + 1) a
insert x Empty = Fork x Empty Empty (Left Refl)
insert x (Fork y (t1 :: BraunTree p a) t2 (Left Refl)) =
  case plusAssoc @p @1 @p of Refl -> -- (p + 1) + p => p + (1 + p)
    case plusComm @1 @p of Refl -> -- p + (1 + p) => p + (p + 1)
      case plusAssoc @p @p @1 of Refl -> -- p + (p + 1) => (p + p) + 1
        Fork x (insert x t1) t2 (Right Refl)

A note: should BraunTree really have two constructors? There are essentially two kinds of Fork: a balanced one and an unbalanced one. It would make a lot more sense (and remove a bunch of indirection) to split Fork into two constructors. It would also be nicer because you would eliminate certain partially-defined values.