#13962: GHCi allows unsaturated type family -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Taken from [http://ics.p.lodz.pl/~stolarek/_media/pl:research:promotion- haskell14-slides.pdf Promoting Functions to Type Families in Haskell] {{{#!hs {-# 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 it 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]`". -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13962 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler