search

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver
Other
16 stars 9 forks source link

Derive 1 <= Max a b when (1 <= a ) or (1 <= b) #41

Open lmbollen opened 2 years ago

lmbollen commented 2 years ago

I'm not sure of this is possible, but it's trival that 1 < = Max a b holds when 1 <= a holds or 1 <= b holds. However, the plugin can't deduce this.

rowanG077 commented 2 years ago

Yes and unfortunately it's not super easy to add. Most reasoning this plugin does is local only. So stuff like using other constraints to solve constraints isn't done.

So instead I solve constraints like this using basic axioms:

maxAxiomL
  :: forall (n :: Nat) (p :: Nat) (q :: Nat)
   . (n <= p) :- (n <= Max p q)
maxAxiomL = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))

and a similar one can be defined for the other case.