Opened 15 months ago

Last modified 3 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 (9)

comment:1 Changed 15 months 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 15 months ago by goldfire

Priority: normalhigh

comment:3 Changed 11 months ago by bgamari

Richard, do you think this will happen for 8.2?

comment:4 Changed 11 months ago by goldfire

ummm... Maybe :)

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

comment:5 Changed 11 months 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 11 months 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 5 months ago by RyanGlScott

Cc: RyanGlScott added

comment:8 Changed 3 months ago by goldfire

Blocked By: 14119 added

comment:9 Changed 3 months ago by goldfire

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

Note: See TracTickets for help on using tickets.