Type family doesn't reduce with visible kind application
If we un-comment f2
{-# Language RankNTypes #-}
{-# Language TypeFamilies #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
import Data.Kind
type family
F1 (a :: Type) :: Type where
F1 a = Maybe a
f1 :: F1 a
f1 = Nothing
type family
F2 :: forall (a :: Type). Type where
F2 @a = Maybe a
-- f2 :: F2 @a
-- f2 = Nothing
this program fails with
• Couldn't match kind ‘forall a1. *’ with ‘* -> *’
When matching types
F2 :: forall a. *
Maybe :: * -> *
Expected type: F2
Actual type: Maybe a
• In the expression: Nothing
In an equation for ‘f2’: f2 = Nothing
|
20 | f2 = Nothing
| ^^^^^^^
Failed, no modules loaded.
It also succeeds replacing Nothing
with undefined
f2 :: F2 @a
f2 = undefined
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | mnguyen |
Operating system | |
Architecture |