[GHC] #14350: Infinite loop when typechecking incorrect implementation (GHC HEAD only)
GHC
ghc-devs at haskell.org
Fri Oct 13 23:41:44 UTC 2017
#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 (Type | Version: 8.3
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:
Old description:
> 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
> | ^^^^^
> }}}
New description:
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 #-}
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
| ^^^^^
}}}
--
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14350#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list