KnownNatN instances are unsafe (in some cases).

[nshepperd]

Found this out while trying to set up unary type level functions. It's a consequence of how we look up an instance's constraints at constraintToEvTerm.go.df_args in the solver. For an instance where the type variables are mentioned in the opposite order to where they appear in the instance head, such as:

forall b a. (KnownNat b, KnownNat a) => DKnownNat2 "+" a b

Suppose we're solving for an instance for KnownNat (x + y). We use piResultTys idType [x, y] to apply the type arguments, but that unfortunately substitutes them in the wrong order, ie. b=x, a=y, resulting in (KnownNat x, KnownNat y) => DKnownNat2 "+" y x when the instance we wanted is (KnownNat y, KnownNat x) => DKnownNat2 "+" x y.

You can see this in action by reversing the order of the KnownNat constraints in the definition of KnownNat2 "-".

I think we want to somehow unify the instance head with KnownNat2 "+" x y in order to properly substitute the type variables and get the right instance, but I'm not familiar with GHC api enough to do that easily.

[christiaanb]

Thanks for the report, I'll take a look at this tonight (GMT).

[christiaanb]

Sorry, spend my time fixing https://ghc.haskell.org/trac/ghc/ticket/11525 (in which I succeeded). I'll try to take another look at this some other time.

[christiaanb]

Ok, I see what's going on. So given the instance head:

instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where

we actually have the implicitly quantified:

instance forall a b . (KnownNat a, KnownNat b, b <= a) => 
  KnownNat2 $(nameToSymbol ''(-)) a b where

However, when we write:

instance (KnownNat b, KnownNat a, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where

we get the implicitly quantified:

instance forall b a . (KnownNat b, KnownNat a, b <= a) => 
  KnownNat2 $(nameToSymbol ''(-)) a b where

Notice the order of the quantifiers.

So now assume the solver is asked to solve `KnownNat (x - y)". In the original it will create evidence for:

[kn1 :: KnownNat x
,kn2 :: KnownNat y
,eq   :: y <= x
]

where we then apply the dictionary function as:

let dfun :: forall a b . KnownNat a -> KnownNat b -> (b <= a) -> SNat (a - b)
in  dfun @x @y kn1 kn2 eq

However, when we have the instance with the reversed quantifiers we do:

let kn1  :: KnownNat y
     kn2 :: KnownNat x
     eq :: (x <= y)
     dfun :: forall b a . KnownNat b -> KnownNat a -> (b <= a) -> SNat (a -b)
in  dfun @x @y kn1 kn2 eq

and the dfun gets its types instantiated in the "wrong" order. Trying to figure out the right order is kind of a hassle. Given how these KnownNatN instances are "magical" anyway, I prefer to just document this fact, and tell people to use explicit quantifiers in their KnownNatN instances. Because when we explicitly write:

instance forall a b . (KnownNat b, KnownNat a, b <= a) => 
  KnownNat2 $(nameToSymbol ''(-)) a b where

everything works.