search

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

Could not deduce `KnownNat (F ((2 * a) + a) b + (2 * F (a + (2 * a)) b))` from `KnownNat (F (a * 3) b * 3)` #47

Open christiaanb opened 4 years ago

christiaanb commented 4 years ago

This happens with:

type family F (a :: Nat) (b :: Nat) :: Nat

proxyEq5
  :: forall a b
   . KnownNat (F (a * 3) b * 3)
  => Proxy a
  -> Proxy b
  -> Proxy (3 * F (3 * a) b)
proxyEq5 = theProxy
 where
  theProxy
    :: forall a b
     . KnownNat (F (2 * a + a) b + (2 * F (a + 2 * a) b))
    => Proxy a
    -> Proxy b
    -> Proxy (3 * F (3 * a) b)
  theProxy _ _ = Proxy

The issue seems to be with http://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/GHC-TcPluginM-Extra.html#v:flattenGivens

because looking at givens + flattened givens I see:

  [[G] $dKnownNat_aCr3 {0}:: KnownNat fsk_aCre[fsk:1] (CDictCan),
   [G] co_aCrd {0}:: F fsk_aCra[fsk:1] b_aCr1[sk:1]
                     GHC.Prim.~# fsk_aCrc[fsk:1] (CFunEqCan),
   [G] co_aCrb {0}:: (a_aCr0[sk:1] * 3)
                     GHC.Prim.~# fsk_aCra[fsk:1] (CFunEqCan),
   [G] co_aCrf {0}:: (fsk_aCrc[fsk:1] * 3)
                     GHC.Prim.~# fsk_aCre[fsk:1] (CFunEqCan),
   [G] $dKnownNat_aCr3 {0}:: KnownNat
                               (F fsk_aCra[fsk:1] b_aCr1[sk:1] * 3) (CDictCan),
   [G] co_aCrd {0}:: F (a_aCr0[sk:1] * 3) b_aCr1[sk:1]
                     GHC.Prim.~# F (a_aCr0[sk:1] * 3) b_aCr1[sk:1] (CFunEqCan),
   [G] co_aCrb {0}:: (a_aCr0[sk:1] * 3)
                     GHC.Prim.~# (a_aCr0[sk:1] * 3) (CFunEqCan),
   [G] co_aCrf {0}:: (F (a_aCr0[sk:1] * 3) b_aCr1[sk:1] * 3)
                     GHC.Prim.~# (F fsk_aCra[fsk:1] b_aCr1[sk:1] * 3) (CFunEqCan)]

where the important given is the flattened:

[G] $dKnownNat_aCr3 {0}:: KnownNat
                               (F fsk_aCra[fsk:1] b_aCr1[sk:1] * 3) (CDictCan),

where fsk_aCra[fsk:1] hasn't been fully expanded