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