Constraint gets lost by enabling the plugin

[kleinreact]

The following example

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}

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

module Test where

import Data.Constraint
import GHC.TypeLits
import Unsafe.Coerce

f :: forall (m :: Nat). SNat m -> SNat (2 * m + 1)
f SNat = SNat

g :: forall n. (1 <= n, n `Mod` 2 ~ 1) => SNat n -> SNat n
g s@SNat | Dict <- divOdd @n = f $ SNat @((n - 1) `Div` 2)

-- evidence that n mod 2 == 1 implies 2 * ((n - 1) div 2) + 1 == n
divOdd :: forall n. (n `Mod` 2 ~ 1, 1 <= n) => Dict ((2 * Div (n - 1) 2) + 1 ~ n)
divOdd = unsafeCoerce (Dict :: Dict (0 ~ 0))

does not type check returning

    • Cannot satisfy: 1 <= n
    • In the second argument of ‘($)’, namely ‘SNat @((n - 1) `Div` 2)’
      In the expression: f $ SNat @((n - 1) `Div` 2)
      In an equation for ‘g’:
          g s@SNat | Dict <- divOdd @n = f $ SNat @((n - 1) `Div` 2)
   |
16 | g s@SNat | Dict <- divOdd @n = f $ SNat @((n - 1) `Div` 2)
   |
   |                                    ^^^^

However, disabling the plugin and introducing the KnownNat constraints manually works, e.g.,

f :: forall (m :: Nat). KnownNat ((2 * m) + 1) => SNat m -> SNat (2 * m + 1)
f SNat = SNat

g :: forall n. (KnownNat (Div (n - 1) 2), 1 <= n, n `Mod` 2 ~ 1) => SNat n -> SNat n
g s@SNat | Dict <- divOdd @n = f $ SNat @((n - 1) `Div` 2)

Note that the reported 1 <= n constraint is obviously given in the type signature, so it seems that it get's lost when the plugin is on.