Opened 2 years ago
Last modified 8 days 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 (16)
comment:1 Changed 2 years ago by
Owner: | set to goldfire |
---|
comment:2 Changed 2 years ago by
Priority: | normal → high |
---|
comment:4 Changed 2 years ago by
ummm... Maybe :)
In reality, probably not. It depends on how my levity polymorphism stuff evolves.
comment:5 Changed 2 years ago by
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 2 years ago by
Milestone: | 8.2.1 → 8.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 20 months ago by
Cc: | RyanGlScott added |
---|
comment:8 Changed 18 months ago by
Blocked By: | 14119 added |
---|
comment:9 Changed 18 months ago by
I've made a new ticket #14119 discussing a refactoring of type patterns. That ticket would solve this one.
comment:10 Changed 5 months ago by
Blocking: | 15515 added |
---|
comment:11 Changed 5 months ago by
Blocking: | 15515 removed |
---|
comment:12 Changed 3 weeks ago by
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 | ^^^^^^^^^^^^^^^^^^
comment:13 Changed 3 weeks ago by
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 forall
s: 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 3 weeks ago by
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 3 weeks ago by
- 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 forF x (G x) = True
, should we ever want to support that.
comment:16 Changed 8 days ago by
A fix for this ticket may also fix #15905. Well, at least the older plan, before comment:12.
Yes. This is a known (but perhaps undocumented) infelicity. I am hoping to fix for 8.2.