Solve `n <= Max (n + p) p` constraints.

[rowanG077]

Should fix issue #28. Like @christiaanb suggested a couple of months back the main change is keeping track of when the solver has normalised something in a constraint. If it has normalised something in a constraint a new wanted constraint is emitted and the original one is marked as solved. I'm not quite sure if this is the way to go since the docs on the API are relatively minimal.

The parts where I'm not sure if I did the right thing are marked as commit comments.

[rowanG077]

I tested compiling clash-prelude in the safe-index branch/pull request with this change and it indeed solves the constraint issue..

[martijnbastiaan]

Nice @rowanG077! I'll have a look after the weekend.

[rowanG077]

@martijnbastiaan ping :)

[rowanG077]

Pong!

Overall, looks good but:

• Could you add a commit message explaining what you did?
• Document the new/changed data types

I'm not terribly excited about even poorer error messages. Do you have a clue to why they've changed? Any idea on how to improve them or at least get it back to its old behavior?

Thanks @martijnbastiaan!

In the old implementation the parts of a constraint that this plugin could normalize are normalized and afterwards a check was performed to try and solve that constraint outright if it was trivial (E.g. 2 <=? 3 ~ 'True). If it was a constraint that is impossible to satisfy an error message is given in terms of the original constraint.

But now when this plugin has normalized a constraint it emits the new constraint and doesn't try to solve it. This means when another part of the type checker now says this constraint is unsolveable it gives it in terms of constraints this plugin has normalized.

I think I can fix it by re-introducing this simple check. This should restore the error messages as they used to be.

[martijnbastiaan]

Clear! Just ping me when you've got that in.

[rowanG077]

@martijnbastiaan It's done.

[christiaanb]

I’d like to test it on one of our commercial code bases. If there’s no regressions, we can merge.

[martijnbastiaan]

I've started a testsuite on a commercial codebase. Results should be in tomorrow!

[martijnbastiaan]

The PR kicks the typecheckers into an infinite loop on the commercial code tested. What can I do to debug this?

[christiaanb]

Reduce to a minimal test case, then run with -ddump-tc-trace on that minimal example. Then see if it keeps printing messages, or halts somewhere.

[martijnbastiaan]

Alright, will do when I've got more time (probably next week, sorry @rowanG077 :()

[rowanG077]

Sucks... Once you have a test case you can post it here and I will do the rest @martijnbastiaan.

[martijnbastiaan]

@rowanG077 I've reduced it to:

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE NoStarIsType        #-}
{-# LANGUAGE TypeOperators       #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver    #-}

module Test where

import GHC.TypeLits
import GHC.TypeLits.Extra

data AB a b where
  AB :: ((CLog 2 a + CLog 2 (2 ^ b)) ~ CLog 2 (a * (2 ^ b))) => AB a b

a :: AB a b -> ()
a AB = b

b :: (KnownNat d, 1 <= d) => f d -> ()
b = undefined

Tested on GHC 8.6.5. It get stuck in an infinite loop of:

Following filled tyvar (zonk_eq_types)
  fsk_a3a0[fsk:2] = fsk_a3a0[fsk:2]
Following filled tyvar (zonk_eq_types)
  fsk_a3a0[fsk:2] = fsk_a3a0[fsk:2]
[...]

Happy hunting :)

[rowanG077]

Thanks that was quick :+1: @martijnbastiaan ! I will see what I can do.

[rowanG077]

I didn't realise that given constraint are also thrown into the solver. This resulted in the bug since given constraints could be normalised and then transformed into wanted constraints and be emitted...

This is fixed now by only emitting a constraint if the original is a wanted constraint. I think the more general approach though is to also emit new given/derived constraints. I tried to do this and nothing broke in the test cases. But I rather keep this PR focused and consider that improvement out of scope.

But I'm a little more nervous now about this change. So please test this again on some larger code bases you have access to!

[christiaanb]

Ah yeah, plugins are called in two phases:

• Phase 1: Collect [G]iven / [D]erived constraints
• Phase 2: Solve [W]anted constraints

You can detect which phase you're in by basically looking whether the list of [W]anted constraints is empty; if it's empty, we're in Phase 1. During Phase 1 you can only emit new [G]iven constraints (or [D]erived constraints); but you shouldn't emit [W]anted constraints.

[martijnbastiaan]

One test has passed, so that's a positive :). Still waiting on the full results.

Should we introduce a (run-time) check if that invariant gets violated then? Could we restructure such that you can't mess it up in the first place?

[christiaanb]

Ah, I misunderstood what went wrong. Yeah, we definitely should not emit [G]iven's as [W]anted's.

Also... we can probably stop putting [G]iven constraints into the solver. I just copy-pasted that aspect from the ghc-typelits-natnormalise plugin, where we do need both the given and wanted constraints, but for this solver doesn't actually extract any information out of the given constraints.

[rowanG077]

@christiaanb Given constraints are used in the plugin to be able to transform constraints of the form q ~ Max x y => (p <=? q ~ True) to (p <=? Max x y) ~ True.

https://github.com/clash-lang/ghc-typelits-extra/blob/487ea1c54c75e49ae56f1f3ced5aabfb1337ac1e/src/GHC/TypeLits/Extra/Solver.hs#L166-L173

[martijnbastiaan]

Nice work @rowanG077. It seems to work just fine at our client's :-).

[rowanG077]

Great! Thanks @martijnbastiaan :+1:!