[GHC] #14720: GHC 8.4.1-alpha regression with TypeInType

[GHC]

#14720: GHC 8.4.1-alpha regression with TypeInType
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.4.1-alpha1
  (Type checker)                     |
           Keywords:  TypeInType     |  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:
-------------------------------------+-------------------------------------
 GHC 8.2.2 is able to typecheck this code:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module SGenerics where

 import Data.Kind (Type)
 import Data.Type.Equality ((:~:)(..), sym, trans)
 import Data.Void

 data family Sing (z :: k)

 class Generic (a :: Type) where
     type Rep a :: Type
     from :: a -> Rep a
     to :: Rep a -> a

 class PGeneric (a :: Type) where
   type PFrom (x :: a)     :: Rep a
   type PTo   (x :: Rep a) :: a

 class SGeneric k where
   sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
   sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)

 class (PGeneric k, SGeneric k) => VGeneric k where
   sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
   sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a

 data Decision a = Proved a
                 | Disproved (a -> Void)

 class SDecide k where
   (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
   default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
                => Sing a -> Sing b -> Decision (a :~: b)
   s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
     Proved (Refl :: PFrom a :~: PFrom b) ->
       case (sTof s1, sTof s2) of
           (Refl, Refl) -> Proved Refl
     Disproved contra -> Disproved (\Refl -> contra Refl)
 }}}

 But GHC 8.4.1-alpha2 cannot:

 {{{
 $ /opt/ghc/8.4.1/bin/ghc Bug.hs
 [1 of 1] Compiling SGenerics        ( Bug.hs, Bug.o )

 Bug.hs:44:52: error:
     • Could not deduce: PFrom a ~ PFrom a
       from the context: b ~ a
         bound by a pattern with constructor:
                    Refl :: forall k (a :: k). a :~: a,
                  in a lambda abstraction
         at Bug.hs:44:37-40
       Expected type: PFrom a :~: PFrom b
         Actual type: PFrom a :~: PFrom a
       NB: ‘PFrom’ is a non-injective type family
     • In the first argument of ‘contra’, namely ‘Refl’
       In the expression: contra Refl
       In the first argument of ‘Disproved’, namely
         ‘(\ Refl -> contra Refl)’
     • Relevant bindings include
         contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
         s2 :: Sing b (bound at Bug.hs:40:9)
         s1 :: Sing a (bound at Bug.hs:40:3)
         (%~) :: Sing a -> Sing b -> Decision (a :~: b)
           (bound at Bug.hs:40:3)
    |
 44 |     Disproved contra -> Disproved (\Refl -> contra Refl)
    |                                                    ^^^^
 }}}

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