Handling of type families is inconsistent with GHC behaviour

[madgen]

Hi,

This is kind of related to #7, but emphasises a different point.

So if we have

f :: b <= T a + b => c
f = undefined

we get a type error and the comment on #7 suggests that is to be cautious about type families that may produce type errors. So I agree with that but GHC doesn't.

As GHC <= does not inspect the right-hand side a constraint of the form 0 <= T a, always type checks. We might argue that this is the wrong behaviour, but that's what GHC does, so perhaps it is not too bad to be consistent with it?

Would you consider a more relaxed approach to handling of stuck type families?

[christiaanb]

I agree that this is a bug, but don't know yet when I'll have time to fix it.

[madgen]

@christiaanb I need it urgently, so if you can point me in the right direction, I can start working on it.

[christiaanb]

@madgen Could you provide a small test case?

I was trying to reproduce what you're saying, but the following compiles fine:

{-# LANGUAGE TypeOperators, DataKinds, GADTs, KindSignatures, TypeFamilies,
             AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits

type family T (a :: Nat) :: Nat

f :: forall b a c . b <= T a + b => c
f = undefined

g :: forall (a :: Nat) c . c
g = f @0 @a @c

I guess I'm misunderstanding the exact issue that you're having

[madgen]

It is so bizarre. When I take it out of the context it occurred, the problem goes way. I still get Could not deduce: (Arity f <=? (NRets r + Arity f)) ~ 'True which I believe is analogous to the problem above. I'll investigate more and update. Sorry about this.

[christiaanb]

@madgen ah... so let's say we have:

type family T (a :: Nat) :: Nat
type family G (a :: Nat) :: Nat

is the following then vacuously true?

G x <= T y + G x

i.e., must the type checker plugin discharge it? Well... it cannot, because we're dealing with natural numbers. Let's say we add the following instances:

type instance T a = a
type instance G a = a - 3

then instantiating:

G x <= T y + G x [x = 2, y = 3]

reduces to:

(2 - 4) <= 3 + (2 - 4)

which gets stuck in GHC, even without the plugin:

{-# LANGUAGE TypeOperators, DataKinds, GADTs, KindSignatures, TypeFamilies,
             AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications,
             UndecidableInstances #-}

import GHC.TypeLits

type family T (a :: Nat) :: Nat

type instance T a = a

type family G (a :: Nat) :: Nat

type instance G a = a - 4

f :: b <= T a + b => c
f = undefined

g :: forall (a :: Nat) (b :: Nat) c . c
g = f @(G 2) @3 @c

with:

Test4.hs:21:5: error:
    • Couldn't match type ‘(2 - 4) <=? (3 + (2 - 4))’ with ‘'True’
        arising from a use of ‘f’
    • In the expression: f @(G 2) @3 @c
      In an equation for ‘g’: g = f @(G 2) @3 @c
   |
21 | g = f @(G 2) @3 @c

[madgen]

@christiaanb I'm a bit confused now, I'm clearly confusing semantics of something. 2 - 4 is 0 in Nat, isn't it? So 0 <=? 3 should be fine?

[christiaanb]

Or {2,4} is simply not in the domain of -. But disregarding -, we also have Div which also doesn’t reduce when the RHS is 0.

[madgen]

Fair. In my case both type families are non-negative, do you think I can convey this information to the type checker/plugin in a useful manner?

[christiaanb]

I guess we could make a class:

class Complete a

instance Complete (+)
instance Complete (*)
instance Complete (^)

And add instances for your type families if you want to assert that: it reduces for any input. Then the plugin could look up instances for this Complete class, and treat applications of those type families as special constants because it knows they won’t get stuck.

But even then.... what if you type family is applied to 2-4 or Div 4 0, then your type family will not reduce, because it argument won’t. Is it still sound to treat them as a natural number?

[madgen]

Well, so going back to my original post, GHC is happy to type check the following:

{-# LANGUAGE TypeOperators, DataKinds, GADTs, KindSignatures, TypeFamilies,
             AllowAmbiguousTypes, ScopedTypeVariables, TypeApplications,
             UndecidableInstances #-}

import GHC.TypeLits

type family G (a :: Nat) :: Nat

type instance G a = a - 4

f' :: 0 <= a => c
f' = undefined

g' :: forall (a :: Nat) (b :: Nat) c . c
g' = f' @(G 2) @c

So, it is already unsound which irks me as well, but if GHC (and consequently your plugin) will do that, I might as well rip its benefits. Does that make sense?

[christiaanb]

I'll add a flag to the plugin by which you can assert that all constants, i.e. F a or F 3 for any type family F :: k -> Nat is a natural number. That way, the plugin will vacuously assert F a <= G a + F a.

[madgen]

Wow, awesome. I didn't see this going as smoothly as it did.

It's a great project by the way. Thank you for making it. Let me know if there are interesting things to do. I'd be interested in helping.

[christiaanb]

I've pushed a commit which adds the flag: 45080a9

With regards to interesting things to do: I would like to extend then inequality solver so that it can handle the expressions in: clash-lang/ghc-typelits-extra#15