Why is UndecidableInstances required for an obviously terminating type family?
In below (working) snippet
{-# 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.
*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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |