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

auto-derive `Div (a * x) a ~ x` #24

Open tscholak opened 5 years ago

tscholak commented 5 years ago

I'd like to define the following:

test :: (1 <= a) => Proxy (Div (n * a) a) -> Proxy n
test = id

However, with -fplugin GHC.TypeLits.Normalise (0.3.1), -fplugin GHC.TypeLits.KnownNat.Solver (0.7), -fplugin GHC.TypeLits.Extra.Solver (0.7),and -fconstraint-solver-iterations=0, ghc 8.6.5 won't have this and complains:

    • Could not deduce: Div (n * a) a ~ n
      from the context: 1 <= a

Is there any way to achieve this?

PS: I can define this:

foo :: forall x n a . (x ~ (n * a)) => Proxy n -> Proxy a -> ()
foo = const . const ()

but this doesn't give me what I need downstream.

christiaanb commented 5 years ago

You can extend this function to get the behavior you want: https://github.com/clash-lang/ghc-typelits-extra/blob/14b52940d30172aee1c315dbc9868c0314017e99/src/GHC/TypeLits/Extra/Solver/Operations.hs#L145

Extend https://github.com/clash-lang/ghc-typelits-extra/blob/14b52940d30172aee1c315dbc9868c0314017e99/src/GHC/TypeLits/Extra/Solver/Operations.hs#L45 with a constructor for multiplication.

And create the mult constructor here: https://github.com/clash-lang/ghc-typelits-extra/blob/14b52940d30172aee1c315dbc9868c0314017e99/src/GHC/TypeLits/Extra/Solver/Unify.hs#L38

And add an extra field for the multiplication tycon here: https://github.com/clash-lang/ghc-typelits-extra/blob/14b52940d30172aee1c315dbc9868c0314017e99/src/GHC/TypeLits/Extra/Solver/Operations.hs#L76

The rest should follow for solving all the type errors.