[GHC] #13774: Singletons code fails to typecheck when type signature involving type family is added

[GHC]

#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