Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,249
    • Issues 5,249
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 573
    • Merge requests 573
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14350
Closed
Open
Issue created Oct 13, 2017 by Ryan Scott@RyanGlScottMaintainer

Infinite loop when typechecking incorrect implementation (GHC HEAD only)

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
   |                           ^^^^^
Edited Mar 10, 2019 by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking