[GHC] #14350: Infinite loop when typechecking incorrect implementation (GHC HEAD only)

[GHC]

#14350: Infinite loop when typechecking incorrect implementation (GHC HEAD only)
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  high           |         Milestone:  8.4.1
          Component:  Compiler       |           Version:  8.3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 On GHC HEAD, typechecking this program loops infinitely:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind

 data Proxy a = Proxy
 data family Sing (a :: k)

 data SomeSing k where
   SomeSing :: Sing (a :: k) -> SomeSing k

 class SingKind k where
   type Demote k :: Type
   fromSing :: Sing (a :: k) -> Demote k
   toSing   :: Demote k -> SomeSing k

 data instance Sing (x :: Proxy k) where
   SProxy :: Sing 'Proxy

 instance SingKind (Proxy k) where
   type Demote (Proxy k) = Proxy k
   fromSing SProxy = Proxy
   toSing Proxy = SomeSing SProxy

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

 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type a @@ b = Apply a b
 infixl 9 @@

 newtype instance Sing (f :: k1 ~> k2) =
   SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }

 instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
   type Demote (k1 ~> k2) = Demote k1 -> Demote k2
   fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing
 sFun y)
   toSing = undefined

 dcomp :: forall (a :: Type)
                 (b :: a ~> Type)
                 (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~>
 c @@ ('Proxy :: Proxy x) @@ y)
                 (g :: forall (x :: a). Proxy x ~> b @@ x)
                 (x :: a).
          Sing f
       -> Sing g
       -> Sing x
       -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
 dcomp f g x = applySing f Proxy Proxy
 }}}

 This is a regression from GHC 8.2.1/8.2.2, where it gives a proper error
 message:

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

 Bug.hs:60:15: error:
     • Couldn't match expected type ‘Proxy a2
                                     -> Apply (Apply (c x4) 'Proxy) (Apply
 (g x4) 'Proxy)’
                   with actual type ‘Sing (f x y @@ t0)’
     • The function ‘applySing’ is applied to three arguments,
       but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
       has only two
       In the expression: applySing f Proxy Proxy
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
         x :: Sing x4 (bound at Bug.hs:60:11)
         g :: Sing (g x3) (bound at Bug.hs:60:9)
         f :: Sing (f x2 y) (bound at Bug.hs:60:7)
         dcomp :: Sing (f x2 y)
                  -> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@
 'Proxy)
           (bound at Bug.hs:60:1)
    |
 60 | dcomp f g x = applySing f Proxy Proxy
    |               ^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:60:27: error:
     • Couldn't match expected type ‘Sing t0’
                   with actual type ‘Proxy a0’
     • In the second argument of ‘applySing’, namely ‘Proxy’
       In the expression: applySing f Proxy Proxy
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
         x :: Sing x4 (bound at Bug.hs:60:11)
         g :: Sing (g x3) (bound at Bug.hs:60:9)
         f :: Sing (f x2 y) (bound at Bug.hs:60:7)
         dcomp :: Sing (f x2 y)
                  -> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@
 'Proxy)
           (bound at Bug.hs:60:1)
    |
 60 | dcomp f g x = applySing f Proxy Proxy
    |                           ^^^^^
 }}}

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