GHC warns an injective type family "may not be injective"
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
data family Sing (a :: k)
data instance Sing (z :: Maybe a) where
SNothing :: Sing Nothing
SJust :: Sing x -> Sing (Just x)
class SingKind k where
type Demote k = r | r -> k
fromSing :: Sing (a :: k) -> Demote k
instance SingKind a => SingKind (Maybe a) where
type Demote (Maybe a) = Maybe (Demote a)
fromSing SNothing = Nothing
fromSing (SJust x) = Just (fromSing x)
f :: forall (x :: forall a. Maybe a) a. SingKind a => Sing x -> Maybe (Demote a)
f = fromSing
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Bug.hs:26:5: error:
• Couldn't match type ‘Demote a’ with ‘Demote a1’
Expected type: Sing (x a) -> Maybe (Demote a1)
Actual type: Sing (x a) -> Demote (Maybe a)
NB: ‘Demote’ is a type function, and may not be injective
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
f :: Sing (x a) -> Maybe (Demote a1) (bound at Bug.hs:26:1)
|
26 | f = fromSing
| ^^^^^^^^
That NB: ‘Demote’ is a type function, and may not be injective
suggestion shouldn't be shown here, since Demote
is definitely injective.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |