A spurious constraint is appearing on my (admittedly tortured) Haskell function. How can I satisfy it?

Question

Playing around with DataKinds in Haskell, I produced the following code, which implements and abuses some type-level unary nats:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Demo where
import Data.Proxy
import Data.Semigroup
import Numeric.Natural
import Data.Constraint

data Nat = Zero | Succ Nat

type family Pred (n :: Nat) where Pred ('Succ n) = n

class IsNat (n :: Nat) where
  nat :: proxy n -> Natural
  unNat :: proxy n -> (n ~ 'Zero => x) -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x) -> x

instance IsNat 'Zero where
  nat _ = 0
  unNat _ z _ = z

instance IsNat n => IsNat ('Succ n) where
  nat _ = succ (nat (Proxy @n))
  unNat _ _ s = s

noneIsNotSuccd :: (n ~ 'Zero, n ~ 'Succ (Pred n)) => proxy n -> a
noneIsNotSuccd _ = error "GHC proved ('Zero ~ 'Succ (Pred 'Zero))!"  -- don't worry, this won't happen

predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

data Indexed (n :: Nat) where
  Z :: Indexed 'Zero
  S :: Indexed n -> Indexed ('Succ n)

instance Show (Indexed n) where
  show Z = "0"
  show (S n) = "S" <> show n

recr :: forall n x. (IsNat n, Semigroup x) => (forall k. IsNat k => Indexed k -> x) -> Indexed n -> x
recr f Z = f Z
recr f (S predn) = predSuccIsNat (Proxy @n) (f predn) <> f (S predn)

main :: IO ()
main = print $ getSum $ recr (Sum . nat) (S Z)

When I attempt to compile it in GHC 8.2.2, I get the following type error:

Demo.hs:35:25: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: forall (n :: Nat) (proxy :: Nat -> *) r.
                                    n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:34:1-96
    • In the expression: unNat proxy (noneIsNotSuccd proxy) r
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |
35 | predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
   |                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is admittedly an improvement over what happens in GHC 8.0.1, where it compiles fine and then fails at runtime:

*** Exception: Demo.hs:34:23: error:
    • Could not deduce (IsNat (Pred n)) arising from a use of ‘unNat’
      from the context: n ~ 'Succ (Pred n)
        bound by the type signature for:
                   predSuccIsNat :: n ~ 'Succ (Pred n) =>
                                    proxy n -> (IsNat (Pred n) => r) -> r
        at Demo.hs:33:1-78
    • In the expression: unNat proxy (noneIsNotSuccd proxy)
      In an equation for ‘predSuccIsNat’:
          predSuccIsNat proxy = unNat proxy (noneIsNotSuccd proxy)
(deferred type error)

It appears that in GHC 8.2.2, unNat is adopting an implicit (IsNat (Pred n)) constraint that does not appear in the type signature:

λ» :t unNat
unNat
  :: IsNat n =>
     proxy n
     -> (n ~ 'Zero => x)
     -> ((n ~ 'Succ (Pred n), IsNat (Pred n)) => x)
     -> x

Is there any way for me to call unNat to implement something like predSuccIsNat?

luqui luqui · Accepted Answer · 2018-01-12T01:03:14

predSuccIsNat :: forall n proxy r. (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r
                        ^^^^^

I don't know where you expect to get the IsNat dictionary that you need in order to use unNat. If I add it to the type signature

predSuccIsNat :: forall n proxy r. IsNat n => (n ~ 'Succ (Pred n)) => proxy n -> (IsNat (Pred n) => r) -> r
predSuccIsNat proxy r = unNat proxy (noneIsNotSuccd proxy) r

everything works fine (on ghc 8.2.1, which has the same deferred problem as 8.0.1).

Without it, it seems like you want to infer that if n ~ 'Succ (Pred n) then IsNat n -- presumably from the fact that Pred n is only defined on Succs. But even if that inference could be made, it would not be enough. For example n ~ Succ m is not enough to infer IsNat either, you would also need IsNat m.

A spurious constraint is appearing on my (admittedly tortured) Haskell function. How can I satisfy it?

1 Answers