"Occurs check" not considered when reducing closed type families

Hello,

consider the following example:

{-# LANGUAGE TypeFamilies #-}

type family Same a b where
  Same a a = Int
  Same a b = Char

example :: Same a [a] -> a
example = undefined

bad :: a
bad = example 'c'

This program should type check, using the following reasoning: a and [a] can never be equal, therefore the first equation for Same does not apply, and so we can fall trough to the second one, thus reducing Same to Char. Therefore, bad should be accept.

GHC rejects this program with the following error:

   • Couldn't match expected type ‘Same a [a]’ with actual type ‘Char’
    • In the first argument of ‘example’, namely ‘'c'’
      In the expression: example 'c'
      In an equation for ‘bad’: bad = example 'c'
    • Relevant bindings include bad :: a (bound at tmp/test.hs:11:1)

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import typechecker labels

What if 'a' was instantiated with Loopy Int where

type family Loop x
type instance Loopy Int = [Loopy Int]

Now indeed if we see Same (Loopy Int) [Loopy Int] we could reduce it to Int.

This is all very tiresome I know. It's discussed at some length in our "Closed type families" paper. If you can think of a better solution than what we propose there, we're all ears.

Simon

Perhaps there is a different way to do the reduction that avoids this problem. My mental model of type functions is that:

1. they only ever ***name*** types, they never introduce ***new*** types, which arise from data, newtype and primitives.
2. they may be partial, so sometimes they don't name any type at all.

I find it easiest to think about all this in terms of GHC's internal representation of the constraints, so your example would look something like this:

(Same a [a] ~ Char, Loop Int ~ a)

Now, I think reducing Same a [a] ~ Char to Char ~ Char, and then just eliminating it as a trivial equality is perfectly valid.

However, eliminating the Loop Int ~ a constraint is what's questionable here, even if a is not used anywhere. This constraint essentially says that Loop Int must be well-defined, in other words, it better refer to an actual ground type that exists.

One (fairly simple?) way for GHC to check the validity of such constraints would be to simply evaluate them until it does find the ground type in question. In your example, this would result in GHC non-terminating during type checking, which is perfectly reasonable, especially since you need UndecidableInstaces to write such recursive types.

Replying to [ticket:11424#comment:113878 diatchki]:

One (fairly simple?) way for GHC to check the validity of such constraints would be to simply evaluate them until it does find the ground type in question. In your example, this would result in GHC non-terminating during type checking, which is perfectly reasonable, especially since you need UndecidableInstaces to write such recursive types.

Except that means that type families can't work over abstract types that we don't know much about yet. For example:

type family Equals a b where
  Equals a a = True
  Equals a b = False

I Equals x x to reduce to True even if I don't know what x is. Under your scheme, I would need to know what x is to be able to make progress, if only to ensure that it terminates.

This whole thing is a sad story. But I don't know how to make it better. See also #10327 and my blog post on the subject (reddit comments on blog post). Bottom line: I think the Right Solution is to require all non-associated type families to be total (implying terminating) and force all non-total type families to be associated with a class constraint. (This actually makes them functional dependencies in disguise!) Then these problems go away.

I am not sure what you mean by "abstract types".

If by x you mean a type variable, then I don't think there is any problem in reducing Equals x x to True.

Otoh, if you encountered Equals (F a) (F a), then you can still reduce that to True, but you'd also have to emit the constraint F a ~ b, to make sure that F a is well-defined.

I do agree that if we can't prove that a type family is total, it essentially should have a well-formedness check on every use---in this example this is F a ~ b, but one may have some other class/constraint encoding the same thing too.

One may also think of this the other way: we always emit a well-formedness constraint on use, but if we've proved that a type function is total, then we can solve this constraint trivially.

Replying to [ticket:11424#comment:113923 diatchki]:

If by x you mean a type variable, then I don't think there is any problem in reducing Equals x x to True.

Otoh, if you encountered Equals (F a) (F a), then you can still reduce that to True, but you'd also have to emit the constraint F a ~ b, to make sure that F a is well-defined.

But this doesn't support the substitution lemma. You say that we can reduce Equals x x. But what if we later learn that x is really F a? So if we're going to do the well-definedness check in the F a case, we have to delay reducing the x case.

I agree with the other points in ticket:11424#comment:113923. Instead of a general well-formedness check, I'm asking the users to provide the name of a class that represents well-formedness.

I don't think that a direct "substitution" lemma makes sense in this context---remember that F a may not refer to a type at all, so we can't just put it in a place where a type is expected.

So, if we had some type-expression t, and wanted to substitute F a for some variable b, we wouldn't do a direct substitution, but rather, we'd emit a new constraint: F a ~ b.

Basically, the idea is that type functions are not really first class types, but may "introduce" types via constraints like: F a ~ b. So, if I write a type like Maybe (F a), what I really mean is (F a ~ b) => Maybe b. Of course, if we can prove that F a is always defined we may "short-cut" the constraint part and just treat it as an ordinary type, but that's optional.

This is basically the same idea is the "functional notation for functional dependencies" (section 3 of "Language and Program Design for Functional Dependencies").

Yes. I think we're vigorously agreeing. Except that this is quite far from the way GHC works at the moment, and it's not a small change to make. I do think it's the right answer, in the end.

added Pnormal label