auto-derive Div (a * x) a ~ x

[tscholak]

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]

You can extend this function to get the behavior you want:

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver/Operations.hs

Line 145 in 14b5294

mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp

Extend

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver/Operations.hs

Line 45 in 14b5294

data ExtraOp

with a constructor for multiplication.

And create the mult constructor here:

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver/Unify.hs

Line 38 in 14b5294

normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp

And add an extra field for the multiplication tycon here:

ghc-typelits-extra/src/GHC/TypeLits/Extra/Solver/Operations.hs

Line 76 in 14b5294

data ExtraDefs = ExtraDefs

The rest should follow for solving all the type errors.