The constraint 0 < d+1 does not seem to resolve?

[noinia]

In the following little code snippet I have to functions, function "libFunc", which has a constraint i < d for two Typelits (e.g. indexing with an index i into some sort of vector of length d). If I use libFunc to index element 0 in a vector of length (d+1) I get the constraint 0 < d+1. This constraint is vacuously true, and hence I was expecting the plugin to resolve this constraint for me. Is this a bug, or was I expecting too much?

I'm using ghc-9.2.4 and ghc-typelits-natnormalise-0.7.7.

{-# LANGUAGE AllowAmbiguousTypes#-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
module Bug where

import GHC.TypeLits
import Data.Type.Ord

libFunc :: forall (i :: Nat) d. i < d => ()
libFunc = ()

-- useFunc :: forall (d :: Nat). 0 < d+1 => () -- with this signature it works
useFunc :: forall (d :: Nat). ()
useFunc = libFunc @0 @(d+1)

[rowanG077]

GHC 9.2 changed a lot of things about how type level comparisons are done. The gist of it is that prior to 9.2 we only had to do reasoning involving <=. GHC changed things to have the entire set of possible comparisons like >, >= and < including a new representation at the type level.

While the plugin was updated to support GHC 9.2 and 9.4 the reasoning it does still only works on <= and not (yet hopefully) on the other inequalites.

See this fragment in the code that only matches on OrdCond (Compare m n) 'True 'True 'False which <=? is aliased to.

ghc-typelits-natnormalise/src-pre-ghc-9.4/GHC/TypeLits/Normalise.hs

Lines 752 to 771 in 127c525

	#if MIN_VERSION_ghc(9,2,0)
	| tc == ordCond
	, [_,cmp,lt,eq,gt] <- xs
	, TyConApp tcCmpNat [x,y] <- cmp
	, tcCmpNat == typeNatCmpTyCon
	, TyConApp ltTc [] <- lt
	, ltTc == promotedTrueDataCon
	, TyConApp eqTc [] <- eq
	, eqTc == promotedTrueDataCon
	, TyConApp gtTc [] <- gt
	, gtTc == promotedFalseDataCon
	, let (x',k1) = runWriter (normaliseNat x)
	, let (y',k2) = runWriter (normaliseNat y)
	, let ks = k1 ++ k2
	= case tc' of
	_ | tc' == promotedTrueDataCon
	-> Just (Right (oCt, (x', y', True)), ks)
	_ | tc' == promotedFalseDataCon
	-> Just (Right (oCt, (x', y', False)), ks)
	_ -> Nothing

The fix(untested) for your code is to rewrite it in terms of <=:

libFunc :: forall (i :: Nat) d. i <= (d - 1) => ()
libFunc = ()

useFunc :: forall (d :: Nat). ()
useFunc = libFunc @0 @(d+1)

[noinia]

Hmm, changing libFunc to have the constraint i <= d-1 indeed allows me to circumvent the issue.

How much work do you expect it to be to include support for the other comparison types? I.e. would that be something that can be fixed relatively "locally" to the lines 751-771 there? E.g. would it be possible to deal with the x < y case by e.g. rewriting x' to whatever the appropriate representation of (1+x') is?

If so I might take a stab at trying to fix that. However, the documentation around what is happening there is somewhat sparse.....

[rowanG077]

Yeah I'd expect you could at least get some rudimentary support for the other operators by just rewriting mechanically to <=. Probably refactor into a separate function as that function is a bit cluttered as is.

Most of the data types you are seeing are from GHC itself which fortunately can be browsed and searched on hackage: https://hackage.haskell.org/package/ghc-9.2.4

You can enable tracing of the type checker with the -ddump-tc-trace GHC option. This will spill lots of useful gibberish of what's happening during type checking to the terminal, including what this plugin is doing. You can find the fragment where this plugin is doing its work by searching for tcPluginSolve start ghc-typelits-natnormalise. You can also add trace expressions in the code yourself using tcPluginTrace.

Generally when I'm working on this codebase I add a single module in tests which only contains the function I'm interested in at this time and enable -ddump-tc-trace only for that module. This way you can limit the output of the type checker trace which makes it much easier to hunt down the interesting parts in the trace.

I think that should be enough information to get started. Good luck if you do try to add support :)!