Opened 10 months ago

Last modified 8 months ago

#15905 new bug

Data familes should end in Type

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

Description

Currently we allow

data family Fix (f :: Type -> k) :: k

with a ‘k’ in the right-hand corner. See Note [Arity of data families] in FamInstEnv.

That seems attractive because we can then have

data instance Fix (f :: Type -> Type -> Type) (x :: Type) = MkFix2 (f (Fix f x) x)

But what about this?

type family F a
type instance F Int = Type -> Type
data instance Fix (f :: Type -> F Int) (x :: Type) = …

The type inference engine (tcInferApps) will type the LHS as something like

	((Fix (f :: Type -> F Int))  |>  co1)
          (x |> co2)

where  co1 :: F Int ~ Type
       co2 :: Type ~ F Int

But the LHS of a family axiom has to look like

	F t1 t2 … tn

not

	((F t1 |> co) t2 t3) |> co4) …tn

with casts in the way. So that LHS must be rejected. And it’s very hard to see how to accept the first example while (predictably, comprehensibly) rejecting the second. It’d be something like “the kind that instantiates k must have obvious, visible, arrows”. Ugh!

And indeed GHC HEAD does accept the first, but rejects the second with the error message

    • Expected kind ‘* -> * -> *’,
        but ‘f :: Type -> F Int’ has kind ‘* -> F Int’
    • In the first argument of ‘Fix’, namely ‘(f :: Type -> F Int)’
      In the data instance declaration for ‘Fix’

That's clearly bogus: we've specified that F Int = Type -> Type. I'm not even sure precisely how it happens, but it must be fragile: a change in solve order, or more aggressive solving might change the behaviour.

I don't see how to solve this. I propose instead to require data family kinds to end in Type, not in a type variable (as we currently allow).

I don't know how many people that would affect, but the current state of affairs looks untenable.

Change History (12)

comment:1 Changed 10 months ago by RyanGlScott

#14645 would be nuked out of existence if this were implemented.

comment:2 Changed 10 months ago by simonpj

Ha ha! I'm in favour of walking (on solid ground) before we run.

comment:3 Changed 10 months ago by goldfire

I don't see any reason to throw the baby out with the bathwater here. It's true that extending this feature to work with type families is difficult, but we can continue the status quo. If we want to make sure that we're order-independent, just look for type families in the instantiated kind. If we spot any, fail.

comment:4 Changed 10 months ago by simonpj

My point is that the status quo is extremely fragile -- it relies crucially on eager unification. It's supposed to be the case that we can defer all unifications to the constraint solver, all all will work. But not so! So now, to give a precise spec, we have to make precise which constraints can be solved eagerly and which can be deferred. I hate that.

The baby is mingled with the bathwater -- it's a fluke that it works at all.

comment:5 Changed 10 months ago by monoidal

Duplicate of #14420?

comment:6 Changed 10 months ago by simonpj

Ah yes. Not quite a duplicate of #14420, but it would nail #14420 inter alia.

In particular, the description of #14420 says (a bit impreciseely) "We should require that any instantiation of a data family be to a kind that ends in Type."

My proposal in this ticket would make that true automatically, because data family kinds would always end in Type, and hence a fortiori so would their instantiations.

comment:7 Changed 9 months ago by bgamari

Milestone: 8.6.3

Ticket retargeted after milestone closed

comment:8 Changed 8 months ago by simonpj

iceland_jack: Ryan thinks you use this feature a lot. Is that true?

comment:9 Changed 8 months ago by RyanGlScott

I'm not Icelandic, but I can provide one "real-world" use case for this feature from the singletons library. It used to be the case that we had about eight or so data types of this shape:

data TyCon1 :: (k1 -> k2) -> (k1 ~> k2)
data TyCon2 :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3)
data TyCon3 :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4)
data TyCon4 :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5)
data TyCon5 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6)
data TyCon6 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7)
data TyCon7 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8)
data TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9)
            -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9)

We arbitrarily capped off the maximum at eight. With the advent of polymorphic data family return kinds, however, we were able to consolidate all of this down into just three things:

data family TyCon :: (k1 -> k2) -> unmatchable_fun

type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where
  ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x)
  ApplyTyCon f x                     = f x

type instance Apply (TyCon f) x = ApplyTyCon f x

Now we don't need to copy-paste TyCon multiple times, and better yet, we don't have to arbitrarily set a maximum of eight, since ApplyTyCon lets us go to whatever arity we desire.

comment:10 Changed 8 months ago by goldfire

Some thoughts from this morning's call:

  • The error report in the original report is unrelated to this ticket: it's just #12088 again. Adding a TH splice does the trick, giving this minimal example:
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TemplateHaskell #-}

module Bug where

import Data.Kind

data family Fix (f :: Type -> k) :: k

type family F a
type instance F Int = Type -> Type

$(return [])

data instance Fix (f :: Type -> F Int) (x :: Type) = Mk

This is accepted, by transforming the instance to

data instance Fix @(Type -> Type) (f :: Type -> Type) (x :: Type) = Mk

In other words, GHC just realizes it can replace F Int with Type -> Type and carry on.

  • In an attempt to stop GHC from being this clever, we tried using visible dependent quantification:
data family Fix k (f :: Type -> k) :: k
data instance Fix (F Int) (f :: Type -> F Int) (x :: Type) = Mk

Note that k is explicit now. This panics, because the unravelFamInstPats chokes on the strange instance, causing downstream chaos. (Really, unravelFamInstPats should panic.) However, if somehow the plumbing were fixed, this would be rejected because it mentions a type family in a type pattern.

  • In another attempt to defeat the ever-clever GHC, I tried using an explicit forall.
data family Fix (f :: Type -> k) :: k
data instance forall (f :: Type -> F Int) (x :: Type). Fix f x = Mk

This works by instantiating Fix with Type -> Type (as before) and casting f.

  • Previously, Simon was worried about the fact that there might be a difference in behavior between eager unification and the work the solver does. But I don't think there is, as solveEqualities is called before unravelFamInstPats.
  • The problem here is really all about when type families get in the way of exposing arrows in the data family's kind. In the Fix example, the type family F Int obscures the underlying type Type -> Type. How do we specify when such a problem exists?
  • I conjecture that the problem never exists on its own. This obfuscation can happen only in two ways: (1) either some kind parameter has been instantiated with a type family application, or (2) a type family application appears in the return kind of a data family. In case (1), we're blocked by #12564; that case cannot happen. In case (2), we're blocked by #14645. So I think that this ticket, by itself, is redundant currently. If either of those other tickets is fixed, it won't be.
  • Fixing #12564 is likely to require generalizing (or otherwise changing) the form of type family LHSs, thus fixing this ticket inter alia.

So, the upshot is: let's fix #12564 before #14645, and this ticket never needs to be considered again. :)

I'm commenting on those two tickets, too.

comment:11 Changed 8 months ago by simonpj

Really, unravelFamInstPats should panic

I agree. Might you find a moment to make it so? Esp now we have a concrete case where chaos happens if we don't.

comment:12 Changed 8 months ago by simonpj

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.