Opened 2 years ago
Last modified 3 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 (11)
comment:1 Changed 2 years ago by
Owner: | set to goldfire |
---|
comment:2 Changed 2 years ago by
Priority: | normal → high |
---|
comment:4 Changed 21 months ago by
ummm... Maybe :)
In reality, probably not. It depends on how my levity polymorphism stuff evolves.
comment:5 Changed 21 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 21 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 15 months ago by
Cc: | RyanGlScott added |
---|
comment:8 Changed 13 months ago by
Blocked By: | 14119 added |
---|
comment:9 Changed 13 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 weeks ago by
Blocking: | 15515 added |
---|
comment:11 Changed 3 weeks ago by
Blocking: | 15515 removed |
---|
Yes. This is a known (but perhaps undocumented) infelicity. I am hoping to fix for 8.2.