GitLab

On GHC HEAD, typechecking this program loops infinitely:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
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:59: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:59:11)                                                       
        g :: Sing (g x3) (bound at Bug.hs:59:9)                                                    
        f :: Sing (f x2 y) (bound at Bug.hs:59:7)                                                  
        dcomp :: Sing (f x2 y)                                                                     
                 -> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)                 
          (bound at Bug.hs:59:1)                                                                   
   |                                                                                               
59 | dcomp f g x = applySing f Proxy Proxy                                                         
   |               ^^^^^^^^^^^^^^^^^^^^^^^                                                         
                                                                                                   
Bug.hs:59: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:59:11)
        g :: Sing (g x3) (bound at Bug.hs:59:9)
        f :: Sing (f x2 y) (bound at Bug.hs:59:7)
        dcomp :: Sing (f x2 y)
                 -> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
          (bound at Bug.hs:59:1)
   |
59 | dcomp f g x = applySing f Proxy Proxy
   |                           ^^^^^