#13774 closed bug (invalid)
Singletons code fails to typecheck when type signature involving type family is added
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | FunDeps, TypeFamilies | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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?
Change History (5)
comment:1 Changed 2 years ago by
Cc: | goldfire added |
---|---|
Keywords: | FunDeps added |
comment:2 Changed 2 years ago by
I don't think this is related to those comments. To explain those comments:
class C a b | a -> b where f :: a -> b class PC a b | a -> b where type F (x :: a) :: b
A use of f
will trigger a need for a C
instance. But a use of F
won't. So, an inference that succeeds on terms fails on types. But that's not what's going on here.
comment:3 Changed 2 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
Your type signature
sT2 :: Sing (L2r 'False)
means
sT2 :: forall k. Sing k (L2r Bool k 'False)
And, since k
is universally quantified, we can't unify it with Nat
. So the instance doesn't match.
You can fix it thus
sT2 :: Sing (L2r 'False :: Nat)
which indeed compiles fine.
I'm not sure what other error message would be better. I'll close as invalid for now.
comment:5 Changed 2 years ago by
Urgh. I'd like to feign ignorance and claim that I would have never thought in a million years to put in a kind ascription, but this isn't even the first time that this bug has bit me (#11275). So I should probably know better by now... but thanks for patiently explaining to me again anyways :)
Some possible wisdom from the
singletons
README:And this comment:
I was unable to dig up anything which explained these comments. Richard, can you elaborate more on this interaction between type families and functional dependencies? Is there an existing ticket which describes the root issue?