search

clash-lang / ghc-typelits-knownnat

Derive KnownNat constraints from other KnownNat constraints
Other
14 stars 10 forks source link

Intermediate type variable stops derivation of `KnownNat` constraint #42

Open rowanG077 opened 2 years ago

rowanG077 commented 2 years ago

Occurs after partially fixing #65 reported in the natnormalise plugin by @lmbollen.

This test:

test29 :: forall a b . (b ~ (2^a)) => SNat a -> SNat (Log b)
test29 SNat = SNat @(Log b)

Fails with:

Could not deduce (KnownNat b) arising from a use of ‘SNat’
    from the context: b ~ (2 ^ a)
      bound by the type signature for:
                 test29 :: forall (a :: Nat) (b :: Nat).
                           (b ~ (2 ^ a)) =>
                           SNat a -> SNat (Log b)
      at tests/Main.hs:187:1-60

Even though it should be able to derive the KnownNat constraint from the KnownNat a given constraint.

rowanG077 commented 2 years ago

I added some logging and the problem is that the substitutions generated from the givens don't lead to the required form. This is the offending type checker trace with stuff that doesn't matter removed:

tcPluginSolve start ghc-typelits-knownnat
  given   = [[G] $dKnownNat_a5Bp {0}:: KnownNat a_a5Bk[sk:1] (CDictCan),
             [G] co_a5DR {1}:: (2 ^ a_a5Bk[sk:1])
                               ghc-prim-0.7.0:GHC.Prim.~# fsk_a5DQ[fsk:1] (CFunEqCan),
             [G] co_a5DS {1}:: fsk_a5DQ[fsk:1]
                               ghc-prim-0.7.0:GHC.Prim.~# b_a5Bl[sk:1] (CTyEqCan)]
  derived = []
  wanted  = [[WD] $dKnownNat_a5DY {0}:: KnownNat
                                          b_a5Bl[sk:1] (CDictCan)]
subst
  [(fsk_a5DQ[fsk:1], 2 ^ a_a5Bk[sk:1]),
   (fsk_a5DQ[fsk:1], b_a5Bl[sk:1])]

kn_wanteds
  [([WD] $dKnownNat_a5DY {0}:: KnownNat b_a5Bl[sk:1] (CDictCan),
    KnownNat,
    b_a5Bl[sk:1],
    Outputable 
    b_a5Bl[sk:1])]

given_map
  [((2 ^ a_a5Bk[sk:1]) ghc-prim-0.7.0:GHC.Prim.~# b_a5Bl[sk:1],
    co_a5DR),
   (b_a5Bl[sk:1] ~ b_a5Bl[sk:1], $d~_a5DT),
   (KnownNat a_a5Bk[sk:1], $dKnownNat_a5Bp),
   ((2 ^ a_a5Bk[sk:1]) ghc-prim-0.7.0:GHC.Prim.~# fsk_a5DQ[fsk:1],
    co_a5DR),
   (fsk_a5DQ[fsk:1] ghc-prim-0.7.0:GHC.Prim.~# b_a5Bl[sk:1], co_a5DS)]

tcPluginSolve ok ghc-typelits-knownnat
  solved = []
  new    = []

kn_wanteds is still KnownNat b_a5Bl[sk:1] even though the plugin can only generate the KnownNat constraint for KnownNat (2 ^ a_a5Bk[sk:1]).

This is because a substitution is not what would be required. We have substitutions:

  [(fsk_a5DQ[fsk:1], 2 ^ a_a5Bk[sk:1]),
   (fsk_a5DQ[fsk:1], b_a5Bl[sk:1]) ]

But we would need (b_a5Bl[sk:1], 2 ^ a_a5Bk[sk:1])

Considering this doesn't go wrong anywhere else I'm not sure why this is happening. If this is limitation of the substitution list we need to make some kind of term rewriting function using the substitutions list as the input and continually rewriting until we get a normal form. Naively this is problematic because rewrites are bidirectional and can form loops. Pinging @christiaanb

rowanG077 commented 2 years ago

See the https://github.com/clash-lang/ghc-typelits-knownnat/tree/fix-42 branch for the additional logging and new test.