#11599: Why is UndecidableInstances required for an obviously terminating type family? -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | 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: -------------------------------------+------------------------------------- In below (working) snippet {{{#!hs {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, UndecidableInstances #-} type family Rev (acc :: [*]) (ts :: [*]) :: [*] where Rev acc '[] = acc Rev acc (t ': ts) = Rev (t ': acc) ts type Reverse ts = Rev '[] ts }}} the `Rev` does an exhaustive pattern match on its second argument and recurses on strictly smaller data. {{{#!hs *Main> :kind! Reverse [Char, Bool, Float] Reverse [Char, Bool, Float] :: [*] = '[Float, Bool, Char] }}} So when I remove `UndecidableInstances` it is not clear to me why this would be rejected :-( {{{ error: The type family application Rev (a : acc) as is no smaller than the instance head (Use UndecidableInstances to permit this) In the equations for closed type family Rev In the type family declaration for Rev Failed, modules loaded: none. }}} I tried this on GHC v8.1.today, but older GHCs behave the same. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11599 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler