Opened 12 years ago

Closed 11 years ago

Last modified 11 years ago

#2235 closed bug (invalid)

Bogus occurs check with type families

Reported by: simonpj Owned by:
Priority: normal Milestone: 6.10 branch
Component: Compiler Version: 6.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider this program, using type families:

    data Even; data Odd

    type family Flip a :: *
    type instance Flip Even = Odd
    type instance Flip Odd = Even

    data List a b where
       Nil  :: List a Even
       Cons :: a -> List a b -> List a (Flip b)

    tailList :: List a b -> List a (Flip b)
    tailList (Cons _ xs) = xs

I get the error (from the HEAD)

    Occurs check: cannot construct the infinite type: b = Flip (Flip b)
    In the pattern: Cons _ xs
    In the definition of `tailList': tailList (Cons _ xs) = xs

There's a bug here -- reporting an occurs check is premature. We should really be able to infer the type

   tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)

But we get the same bogus occurs-check error with this signature.

This example also illustrates why we might want closed families. If you look at the type constraints arising from tailList you'll see that you get (c ~ Flip b, b ~ Flip c) where c is the existential you get from the GADT match. Now, we know that b = Flip (Flip b) is always true, but GHC doesn't. After all, you could add new type instances

	type instance Flip Int = Bool
   	type instance Flip Bool = Char

and then the equation wouldn't hold. What we really want is a *closed* type family, like this

	type family Flip a where
		Flip Even = Odd
		Flip Odd = Even

(preferably supported by kinds) and even *then* it's not clear whether it's reasonable to expect the compiler to solve the above problem by trying all possiblities. This relates to #2101

Change History (5)

comment:1 Changed 11 years ago by igloo

Milestone: 6.10 branch

comment:2 Changed 11 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:3 Changed 11 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:4 Changed 11 years ago by chak

Resolution: invalid
Status: newclosed

We agreed that this

tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)

is not the right signature.

The new solver doesn't produce the infinite-type error message, but the usual one where it complains about not being able to instantiate a rigid type.

comment:5 Changed 11 years ago by simonpj

Just to fill in the details here. The type of Cons is

Cons :: forall a b. forall c. (b ~ Flip c) => a -> List a c -> List a b

The task is this:

b ~ Flip (Flip b), b ~ Flip c  |-  List a (Flip b) ~ List a c

And indeed that isn't provable. If we'd written the type of Cons the other way about, thus:

Cons :: forall a b. a -> List a (Flip b) -> List a b

then we could prove it; but doubtless something else would go wrong. To do it right we'd have to give this type to Cons

Cons :: forall a b c. (b ~ Flip c, c ~ Flip b) => a -> List a c -> List a b

Which we could. But it seems uncomfortably fragile.

Simon

Note: See TracTickets for help on using tickets.