[GHC] #13774: Singletons code fails to typecheck when type signature involving type family is added
GHC
ghc-devs at haskell.org
Thu Jun 1 04:57:30 UTC 2017
#13774: Singletons code fails to typecheck when type signature involving type
family is added
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
(Type checker) |
Keywords: TypeFamilies | Operating System: Unknown/Multiple
Architecture: | Type of failure: GHC rejects
Unknown/Multiple | valid program
Test Case: | Blocked By:
Blocking: | Related Tickets:
Differential Rev(s): | Wiki Page:
-------------------------------------+-------------------------------------
Yes, I know "singletons" is in the title... but the code isn't //that//
scary, I promise. Here's some code which //does// typecheck:
{{{#!hs
{-# 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:
{{{#!hs
sT2 :: Sing 'Zero
sT2 = sL2r SFalse
}}}
However, if you give it either of these two type signatures:
{{{#!hs
sT2 :: Sing T2
}}}
{{{#!hs
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?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13774>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list