search

clash-lang / ghc-typelits-knownnat

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

KnownNat (x*y*x) erroneously solved to KnownNat (x^2) #10

Closed christiaanb closed 7 years ago

christiaanb commented 7 years ago 
test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer
test22 _ _ = natVal (Proxy :: Proxy (y*x*y))
> test22 (Proxy @3) (Proxy @4)
16
ggreif commented 7 years ago

Wow, nasty. Sounds like asserting that after finding out the unknowns and substituting them back into the original equation the proposition should still hold would be a good idea.