Type equality constraints aren't used by solver

[gergoerdi]

The following code fails to typecheck:

{-# LANGUAGE GADTs, ScopedTypeVariables, DataKinds, KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Rank2Types #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

import Data.Singletons.Prelude.Num
import Data.Singletons
import GHC.TypeLits

data Foo :: Nat -> * where
  FZ  :: Foo 0
  FS :: Foo n -> Foo (n + 1)

sPred :: (KnownNat n) => Sing (n+1) -> Sing n
sPred _ = sing

foo :: forall a n. (KnownNat n) => a -> (forall m. KnownNat m => Sing m -> a) -> Foo n -> a
foo x0 f = go (sing :: Sing n)
  where
    go :: forall k. (KnownNat k) => Sing k -> Foo k -> a
    go s FZ = x0
    go s (FS _) = f (sPred s)

The error message is as follows (on GHC 8.0.2):

KnownNatSolverBug.hs:25:19: error:
    * Could not deduce (KnownNat n1) arising from a use of `f'
      from the context: KnownNat n
        bound by the type signature for:
                   foo :: KnownNat n =>
                          a -> (forall (m :: Nat). KnownNat m => Sing m -> a) ->
        at KnownNatSolverBug.hs:20:1-91
      or from: KnownNat k
        bound by the type signature for:
                   go :: KnownNat k => Sing k -> Foo k -> a
        at KnownNatSolverBug.hs:23:5-56
      or from: k ~ (n1 + 1)
        bound by a pattern with constructor:
                   FS :: forall (n :: Nat). Foo n -> Foo (n + 1),
                 in an equation for `go'
        at KnownNatSolverBug.hs:25:11-14
      Possible fix:
        add (KnownNat n1) to the context of the data constructor `FS'
    * In the expression: f (sPred s)
      In an equation for `go': go s (FS _) = f (sPred s)
      In an equation for `foo':
          foo x0 f
            = go (sing :: Sing n)
            where
                go :: forall k. (KnownNat k) => Sing k -> Foo k -> a
                go s FZ = x0
                go s (FS _) = f (sPred s)

To highlight, the relevant parts of the context are:

    * Could not deduce (KnownNat n1) arising from a use of `f'
      from: KnownNat k
      or from: k ~ (n1 + 1)

But isn't this exactly the situation that the plugin was designed to handle?

[gergoerdi]

Actually foo above can be simplified further to just:

foo :: forall a n. (KnownNat n) => a -> (forall m. KnownNat m => Sing m -> a) -> Sing n -> Foo n -> a
foo x0 f s FZ = x0
foo x0 f s (FS _) = f (sPred s)

KnownNatSolverBug.hs:22:21: error:
    * Could not deduce (KnownNat n1) arising from a use of `f'
      from the context: KnownNat n
      or from: n ~ (n1 + 1)

[christiaanb]

Thanks for the report, and simple test case. I'll try to look into this over the weekend.

[gergoerdi]

The following example, even simpler, cuts right to the crux of the issue:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE Rank2Types, FlexibleContexts #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

import Data.Singletons
import GHC.TypeLits

bar :: (KnownNat n, n ~ (m+1)) => (forall k. KnownNat k => Sing k -> a) -> Sing m -> a
bar f s = f s

bug.hs:11:11: error:
    • Could not deduce (KnownNat m) arising from a use of ‘f’
      from the context: (KnownNat n, n ~ (m + 1))

[gergoerdi]

I strongly believe that this is because offset, in constraintToEvTerm, doesn't handle the case when classifyPredType ty' returns an EqPred instead of a ClassPred.

[gergoerdi]

Of course, it's tricky if we also want to support chains of equalities like in

bar :: (KnownNat k, k ~ (n+1), n ~ (m+1)) => (forall x. KnownNat x => Sing x -> a) -> Sing m -> a
bar f s = f s

so it seems that from the EqPreds, we'd need to interpret the semantics of the equalities somehow, it's not just a matter of mere syntactic transformation like rewriting by all equalities.

[christiaanb]

{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver   #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise         #-}
{-# OPTIONS_GHC -dcore-lint #-}

module EqTest where

import GHC.TypeLits

foo :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer
foo m = natVal m

works with the above mentioned patch

[kozross]

Just ran into a similar issue:

{-# LANGUAGE AllowAmbiguousTypes, DataKinds, TypeFamilies, TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -dcore-lint #-}

module EqTest where

import Numeric.Natural
import GHC.TypeNats

foo :: (KnownNat n, KnownNat m, k ~ (n + m)) => proxy k -> Natural
foo = natVal

This produces the following error:

src/EqTest.hs:12:7: error:
    • Could not deduce (KnownNat k) arising from a use of ‘natVal’
      from the context: (KnownNat n, KnownNat m, k ~ (n + m))
        bound by the type signature for:
                   foo :: forall (n :: Nat) (m :: Nat) (k :: Nat) (proxy :: Nat -> *).
                          (KnownNat n, KnownNat m, k ~ (n + m)) =>
                          proxy k -> Natural
        at src/EqTest.hs:11:1-66
      Possible fix:
        add (KnownNat k) to the context of
          the type signature for:
            foo :: forall (n :: Nat) (m :: Nat) (k :: Nat) (proxy :: Nat -> *).
                   (KnownNat n, KnownNat m, k ~ (n + m)) =>
                   proxy k -> Natural
    • In the expression: natVal
      In an equation for ‘foo’: foo = natVal
   |
12 | foo = natVal
   |       ^^^^^^

I'm on GHC 8.6.5, and using ghc-typelits-knownnat and ghc-typelits-natnormalise version 0.7.

[christiaanb]

@kozross @sheaf I acknowledge the existence of this bug / missing feature; sadly, I don't have a lot of time to fix it right now.