Opened 3 years ago

Last modified 7 months ago

#12564 new bug

Type family in type pattern kind

Reported by: int-index Owned by: goldfire
Priority: high Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType, TypeFamilies Cc: goldfire, int-index, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: #14119 Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I want to write a type family that is analogous to !! for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:

{-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}

import Data.Kind

data N = Z | S N

type family Len (xs :: [a]) :: N where
  Len '[] = Z
  Len (_ ': xs) = S (Len xs)

data Fin :: N -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
  At (x ': _) FZ = x
  At (_ ': xs) (FS i) = At xs i

It fails to compile with this error:

FinAt.hs:16:3: error:
    • Illegal type synonym family application in instance: 'FZ
    • In the equations for closed type family ‘At’
      In the type family declaration for ‘At’

That's because the kind of the FZ pattern (first clause of At) has the kind Fin (Len xs) and the application of Len cannot reduce completely. checkValidTypePat then disallows the pattern, as it contains a type family application.

I tried to suppress checkValidTypePat and the definition of At has compiled; however, it's of little use, since At doesn't reduce:

x :: At '[Bool] FZ
x = True

results in

FinAt.hs:20:5: error:
    • Couldn't match expected type ‘At
                                      * ((':) * Bool ('[] *)) ('FZ 'Z)’
                  with actual type ‘Bool’
    • In the expression: True
      In an equation for ‘x’: x = True

Change History (19)

comment:1 Changed 3 years ago by goldfire

Owner: set to goldfire

Yes. This is a known (but perhaps undocumented) infelicity. I am hoping to fix for 8.2.

comment:2 Changed 3 years ago by goldfire

Priority: normalhigh

comment:3 Changed 3 years ago by bgamari

Richard, do you think this will happen for 8.2?

comment:4 Changed 3 years ago by goldfire

ummm... Maybe :)

In reality, probably not. It depends on how my levity polymorphism stuff evolves.

comment:5 Changed 3 years ago by int-index

In reality, probably not

:(

I'd love to see a fix for this in 8.2 - tell me if I can assist.

comment:6 Changed 3 years ago by bgamari

Milestone: 8.2.18.4.1

In that case I'll bump this off to 8.4. Do feel free to bump it back if things change, however.

comment:7 Changed 2 years ago by RyanGlScott

Cc: RyanGlScott added

comment:8 Changed 2 years ago by goldfire

Blocked By: 14119 added

comment:9 Changed 2 years ago by goldfire

I've made a new ticket #14119 discussing a refactoring of type patterns. That ticket would solve this one.

comment:10 Changed 13 months ago by RyanGlScott

Blocking: 15515 added

comment:11 Changed 13 months ago by monoidal

Blocking: 15515 removed

comment:12 Changed 8 months ago by simonpj

Current error message is a bit better

T12564.hs:18:3: error:
    • Illegal type synonym family application ‘Len @a _1’ in instance:
        At @a ((':) @a x _1) ('FZ @(Len @a _1))
    • In the equations for closed type family ‘At’
      In the type family declaration for ‘At’
   |
18 |   At (x ': _) FZ = x
   |   ^^^^^^^^^^^^^^^^^^
Last edited 8 months ago by simonpj (previous) (diff)

comment:13 Changed 8 months ago by goldfire

I have an approach here worth documenting. In brief: flatten equations' left-hand sides, emitting constraints during reduction.

Here is how the example in the OP would work. Original equation:

  At (x ': _) FZ = x

with implicit things made explicit:

  At @a ((:) @a x _1) (FZ @(Len @a _1)) = x

But now, we flatten. By this, I mean we take all type family applications on the LHS and convert them into variables, and assert equality constraints that the variables equal the original type family applications. To wit:

  (m ~ Len @a _1) => At @a ((:) @a x _1) (FZ @m) = x

This yields a constrained type family equation. (Note: this is mostly unrelated to Constrained Type Families) During reduction, this equation would match a target regardless of the (implicit) argument to FZ, but the matcher would then emit a constraint asserting that this argument equals Len @a _1. It's quite like how class instance matching works: we match against the head, emitting any instance constraints.

Type family equations give rise to axioms in Core. To keep type safety, we would need these axioms to take the evidence of the equality match as arguments. Continuing our example, we would get this axiom:

axAt :: forall (a :: Type) (x :: a) (_1 :: [a]) (m :: Nat).
        forall (cv :: m ~ Len @a _1).
        At @a ((:) @a x _1) (FZ @m) ~ x

Note that there are two foralls: the first binds type variables and the second binds coercion variables. In this case, the coercion variable cv is unused in the RHS, but it might potentially be mentioned.

This equation could be used to reduce At ["a", "b", "c"] FZ to "a". We would use the instantiated axiom

axAt Symbol "a" ["b", "c"] 2 coLen :: At ["a", "b", "c"] FZ ~ "a"

where coLen :: 2 ~ Len ["b", "c"] is built from the axioms that describe the behavior of Len.

Note that there is already some infrastructure for this: the cvs in CoAxBranch (and a few other places nearby) are exactly these coercion variables. What's remaining to do is to perform the flattening pass that inserts the cvs and to teach the type-family reduction mechanism (in TcFlatten) to emit the constraints. One challenge is that sometimes (normaliseType) we reduce type families without the ability to solve constraints, so some care must be taken there. However, these cases are outside our usual pipeline and can be special-cased. (While implementing -XTypeInType, I did this once upon a time, so I know it's possible.)

comment:14 Changed 8 months ago by simonpj

Generally I like this. But:

  • We'd need to update the dynamic semantics and subject-reduction proof for FC to show that the resulting system is sound.
  • I'm very troubled by the fact that the evidence is not used. It's all very similar to class instances, except that in class instances we use the evidence.
  • You way that the "evidence may potentially be mentioned" but how might that happen?
  • In the example here we know for certain that the evidence is redundant. The (Len @a _1) was not written by the user; it was inferred. GHC never guesses, so it must be uniquely determined. So it's really a waste of time to construct and pass that evidence at every call site.

Surely there must be a solid criterion for what components of the type are fully determined, and hence redundant and don't need to be matched?

comment:15 Changed 8 months ago by goldfire

  • Bizarrely, I don't think we need to do much proving. The type safety proof depends on the non-overlap of axiom LHSs. That's unchanged here -- the overlap check must treat any type family application on an LHS just like it would a variable. The equality constraints serve only to reduce the applicability of axioms, never to increase it. Thus, no threats to safety.
  • But the evidence is used: it's passed to the coercion axiom. The evidence is the coLen in my example above.
  • I take back the "evidence may be mentioned" comment.
  • GHC passes loads of redundant information at every call site (e.g. id @Bool True). This is not new. The uniquely-determined check would help those other places too. I think, in the end, that idea is orthogonal to the plan here, which would work for F x (G x) = True, should we ever want to support that.

comment:16 Changed 8 months ago by goldfire

A fix for this ticket may also fix #15905. Well, at least the older plan, before comment:12.

comment:17 Changed 7 months ago by RyanGlScott

For anyone reading this ticket who is searching for a workaround:

While I haven't found a general-purpose way to avoid this bug, in limited situations it's often possible to rewrite your type families in a way that shifts applications of type families from the left-hand side to the right-hand side. For example, GHC does accept this formulation of At:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Type.Equality

data N = Z | S N

type family Len (xs :: [a]) :: N where
  Len '[] = Z
  Len (_ ': xs) = S (Len xs)

data Vec :: N -> Type -> Type where
  VNil :: Vec Z a
  (:>) :: a -> Vec n a -> Vec (S n) a

type family ListToVec (l :: [a]) :: Vec (Len l) a where
  ListToVec '[]    = VNil
  ListToVec (x:xs) = x :> ListToVec xs

data Fin :: N -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
  At xs i = At' (ListToVec xs) i

type family At' (xs :: Vec n a) (i :: Fin n) :: a where
  At' (x :> _)  FZ     = x
  At' (_ :> xs) (FS i) = At' xs i

-- Unit tests
test1 :: At '[True] FZ :~: True
test1 = Refl

test2 :: At [True, False] FZ :~: True
test2 = Refl

test3 :: At [True, False] (FS FZ) :~: False
test3 = Refl

If you inspect the definition of At, you'll see why this works:

λ> :info At
type family At @a (xs :: [a]) (i :: Fin (Len @a xs)) :: a where
  forall a (xs :: [a]) (i :: Fin (Len @a xs)).
    At @a xs i = At' @(Len @a xs) @a (ListToVec @a xs) i

Note that the left-hand side, At @a xs i, does not contain any immediate uses of Len. (The kind of i does, but thankfully, GHC doesn't consider that to be an illegal type synonym family application.) The other uses of Len and ListToVec have been quarantined off on the right-hand side, where GHC can't complain about them.

comment:18 Changed 7 months ago by RyanGlScott

The trick from comment:17 can be further generalized to a pseudo-algorithm that (I think) would work for any closed type family that suffers from this problem. Here is what you have to do:

  1. Identity any "problematic" type families that cause the Illegal type synonym family application in instance error. In the original example, the only problematic type family is Len.
  2. Encode each problematic type families as an inductive proposition. In the particular case of Len, this would look this like:
data LenProp :: forall a. [a] -> N -> Type where
  LenNil  :: LenProp '[] Z
  LenCons :: LenProp xs n -> LenProp (x:xs) (S n)

The type family's argument kinds (e.g., [a]) as well as the return kind (e.g., N) become part of the proposition's kind. Each constructor encodes a single equation of the type family. The LenNil constructor encodes the Len '[] = Z equation, and its return type of LenProp '[] Z encodes the fact that this equation takes '[] as an argument and returns Z. Similarly, the LenCons constructor encodes the Len (_ ': xs) = S (Len xs) equation, and the field of type LenProp xs n encodes the recursive call to Len on the right-hand side of the equation. Notice that we "bind" the result of this recursive call to n and use S n in the return type, since the equation applies S to the recursive Len call.

  1. Take all type families that were rejected previously due to occurrences of problematic type families and define "internal" versions of them using the newly defined proposition types. In the particular case of At, this would look this:
type family At' (xs :: [a]) (lp :: LenProp xs r) (i :: Fin r) :: a where
  At' (x:_)  (LenCons _)  FZ     = x
  At' (_:xs) (LenCons lp) (FS i) = At' xs lp i

Note that Len does not appear anywhere in this definition. Where we previously had Fin (Len xs) we now have Fin r, where the r is bound by a new argument of kind LenProp xs r. In general, you'll need to introduce as many new arguments with proposition kinds as is necessary to replace all occurrences of problematic type families.

  1. For each proposition-encoded type family, define another type family that translates the arguments of the original type family to the corresponding proposition. For example, the following type family translates a list to a LenProp:
type family EncodeLenProp (xs :: [a]) :: LenProp xs (Len xs) where
  EncodeLenProp '[]    = LenNil
  EncodeLenProp (_:xs) = LenCons (EncodeLenProp xs)

Note the return kind of LenProp xs (Len xs). This is important, since this is how we are going to "sneak in" a use of Len into At in the next step. Note that Len is not problematic in EncodeLenProp itself since Len never worms its way into a left-hand-side argument.

  1. Finally, redefine type families in terms of the "internal" ones created in step (3). In the particular case of At, it would become:
type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
  At xs i = At' xs (EncodeLenProp xs) i

This uses EncodeLenProp to sneak a use of Len into At'. Critically, this definition avoids pattern-matching on i (since that would trigger the Illegal type synonym family application in instance error). All that At does now is pass its arguments along to At', which does the real work on the proposition created by EncodeLenProp. In this version of At, the only place where Len occurs on the left-hand side is in the kind of i, which GHC deems acceptable.

My program in comment:17 essentially follows the algorithm above, except it uses a slightly more complicated type, Vec, instead of LenProp.


This seems to work for all of the closed type families that I've encountered that suffer from this issue. That being said, this trick doesn't really work well in the setting of open type families, as it's not always possible to know a priori which kind arguments in an open type family might end up being instantiated with type families. If you figure out a general workaround for that, let me know :)

comment:19 Changed 7 months ago by RyanGlScott

After reading comment:13, I'm left wondering about how this idea would work in practice. I've wanted to define instances like these before:

type family Sing :: k -> Type

type instance Sing @Type     = TypeRep
type instance Sing @(Sing a) = Sing

Currently, GHC prevents me from writing the Sing @(Sing a) instance since its argument mentions the Sing type family. If I understand the plan in comment:13, then GHC would turn this instance into something that looks roughly like this:

type instance (x ~ Sing a) => Sing @x = Sing

However, this might be a problem. We have both a Sing @x and a Sing @Type instance defined—wouldn't these instances conflict?

Note: See TracTickets for help on using tickets.