Skip to content

Some type family in the codomain of another type family seems to get stuck

Steps to reproduce

I expect this example (minimized from an attempt to implement recursion-schemes with type families) to typecheck, but it fails with the error below:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Data.Kind ( Type )

type family Base (t :: Type) :: Type -> Type
type instance Base [a] = ListF a

type family Project (t :: a) :: Base a a
type instance Project '[] = 'NilF

data ListF a b = ConsF a b | NilF
Main.hs:15:29: error:
    • Expected kind ‘Base [k0] [k0]’,
        but ‘'NilF’ has kind ‘ListF a0 [k0]’
    • In the type ‘'NilF’
      In the type instance declaration for ‘Project’
   |
15 | type instance Project '[] = 'NilF
   |                             ^^^^^

Expected behavior

We should have Base [k0] [k0] = ListF k0 [k0] so the above should succeed. A visible type application on NilF to pin down its type does not help.

Environment

  • GHC version used: 8.10.3
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information