Skip to content

GHCi allows unsaturated type family

Taken from Promoting Functions to Type Families in Haskell

{-# Language TypeFamilies, PolyKinds, DataKinds, TypeOperators #-}

type family
  Map (f :: a -> b) (xs :: [a]) :: [b] where
  Map f '[]       = '[]
  Map f (x ': xs) = f x ': Map f xs

data N = O | S N

type family
  Pred (n :: N) :: N where
  Pred O     = O
  Pred (S n) = n

-- The type family ‘Map’ should have 2 arguments, but has been given 1
type MapPred = Map Pred

fails as expected, but commenting it out and writing Map Pred works in GHCi

ghci> :kind Map Pred
Map Pred :: [N] -> [N]
ghci> :kind! Map Pred '[S (S O), S O, O]
Map Pred '[S (S O), S O, O] :: [N]
= '['S 'O, 'O, 'O]

I can only test this in GHC 7.8, 8 now. I know GHCi has weird rules for unsaturated type families but I figured I'd write a ticket because the slides say "But it is invalid to write: Map Pred '[O, S O]".

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information