Singletons code fails to typecheck when type signature involving type family is added
Yes, I know "singletons" is in the title... but the code isn't //that// scary, I promise. Here's some code which //does// typecheck:
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data family Sing (a :: k)
data Nat = Zero | Succ Nat
data instance Sing (b :: Bool) where
SFalse :: Sing 'False
STrue :: Sing 'True
data instance Sing (n :: Nat) where
SZero :: Sing 'Zero
SSucc :: Sing n -> Sing ('Succ n)
type family Not (x :: Bool) :: Bool where
Not 'True = 'False
Not 'False = 'True
sNot :: Sing b -> Sing (Not b)
sNot STrue = SFalse
sNot SFalse = STrue
class PFD a b | a -> b where
type L2r (x :: a) :: b
instance PFD Bool Nat where
type L2r 'False = 'Zero
type L2r 'True = 'Succ 'Zero
type T2 = L2r 'False
class SFD a b | a -> b where
sL2r :: forall (x :: a). Sing x -> Sing (L2r x :: b)
instance SFD Bool Nat where
sL2r SFalse = SZero
sL2r STrue = SSucc SZero
sT2 = sL2r SFalse
It also typechecks if you give sT2
this particular type signature:
sT2 :: Sing 'Zero
sT2 = sL2r SFalse
However, if you give it either of these two type signatures:
sT2 :: Sing T2
sT2 :: Sing (L2r 'False)
Then GHC 8.0.1, 8.0.2, 8.2.1, and HEAD will choke:
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:46:7: error:
• No instance for (SFD Bool k) arising from a use of ‘sL2r’
• In the expression: sL2r SFalse
In an equation for ‘sT2’: sT2 = sL2r SFalse
|
46 | sT2 = sL2r SFalse
| ^^^^^^^^^^^
At this point, I get the urge to yell obscenities at GHC, because there definitely //is// an instance of the form SFD Bool k
in scope (and moreover, SFD
's functional dependency should make sure that k ~ Nat
). Shouldn't it be using that?
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |