[GHC] #14203: GHC-inferred type signature doesn't actually typecheck

[GHC]

#14203: GHC-inferred type signature doesn't actually typecheck
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This code typechecks:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind

 data TyFun :: * -> * -> *
 type a ~> b = TyFun a b -> *
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 data family Sing :: k -> *

 data Sigma (a :: *) :: (a ~> *) -> * where
   MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
              Sing x -> Apply p x -> Sigma a p

 data instance Sing (z :: Sigma a p) where
   SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)
 }}}

 I was curious to know what the full type signature of `SMkSigma` was, so I
 asked GHCi what the inferred type is:

 {{{
 λ> :i SMkSigma
 data instance Sing z where
   SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
                                                        x) (px :: Apply p
 x).
               (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)
 }}}

 I attempted to incorporate this newfound knowledge into the program:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module Bug where

 import Data.Kind

 data TyFun :: * -> * -> *
 type a ~> b = TyFun a b -> *
 infixr 0 ~>

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 data family Sing :: k -> *

 data Sigma (a :: *) :: (a ~> *) -> * where
   MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
              Sing x -> Apply p x -> Sigma a p

 data instance Sing (z :: Sigma a p) where
   SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply
 p x).
               Sing sx -> Sing px -> Sing (MkSigma sx px)
 }}}

 But to my surprise, adding this inferred type signature causes the program
 to no longer typecheck!

 {{{
 GHCi, version 8.3.20170907: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:23:31: error:
     • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
     • In the first argument of ‘Sing’, namely ‘px’
       In the type ‘Sing px’
       In the definition of data constructor ‘SMkSigma’
    |
 23 |               Sing sx -> Sing px -> Sing (MkSigma sx px)
    |                               ^^
 }}}

 I'm showing the output of GHC HEAD here, but this bug can be reproduced
 all the way back to GHC 8.0.1.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14203>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler