Type family in type pattern kind
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:
```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:
```haskell
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
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, int-index |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Type family in type pattern kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","int-index"],"type":"Bug","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:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #-}\r\n\r\nimport Data.Kind\r\n\r\ndata N = Z | S N\r\n\r\ntype family Len (xs :: [a]) :: N where\r\n Len '[] = Z\r\n Len (_ ': xs) = S (Len xs)\r\n\r\ndata Fin :: N -> Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n -> Fin (S n)\r\n\r\ntype family At (xs :: [a]) (i :: Fin (Len xs)) :: a where\r\n At (x ': _) FZ = x\r\n At (_ ': xs) (FS i) = At xs i\r\n}}}\r\n\r\nIt fails to compile with this error:\r\n\r\n{{{\r\nFinAt.hs:16:3: error:\r\n • Illegal type synonym family application in instance: 'FZ\r\n • In the equations for closed type family ‘At’\r\n In the type family declaration for ‘At’\r\n}}}\r\n\r\nThat'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.\r\n\r\nI tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:\r\n\r\n{{{#!haskell\r\nx :: At '[Bool] FZ\r\nx = True\r\n}}}\r\n\r\nresults in\r\n\r\n{{{\r\nFinAt.hs:20:5: error:\r\n • Couldn't match expected type ‘At\r\n * ((':) * Bool ('[] *)) ('FZ 'Z)’\r\n with actual type ‘Bool’\r\n • In the expression: True\r\n In an equation for ‘x’: x = True\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->
issue