Opened 13 months ago
Last modified 5 weeks 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 (9)
comment:1 Changed 13 months ago by
Owner: | set to goldfire |
---|
comment:2 Changed 13 months ago by
Priority: | normal → high |
---|
comment:4 Changed 9 months ago by
ummm... Maybe :)
In reality, probably not. It depends on how my levity polymorphism stuff evolves.
comment:5 Changed 9 months 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 9 months 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 3 months ago by
Cc: | RyanGlScott added |
---|
comment:8 Changed 5 weeks ago by
Blocked By: | 14119 added |
---|
comment:9 Changed 5 weeks ago by
I've made a new ticket #14119 discussing a refactoring of type patterns. That ticket would solve this one.
Yes. This is a known (but perhaps undocumented) infelicity. I am hoping to fix for 8.2.