#14350 closed bug (fixed)
Infinite loop when typechecking incorrect implementation (GHC HEAD only)
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.4.1 |
Component: | Compiler (Type checker) | Version: | 8.3 |
Keywords: | TypeInType | Cc: | simonpj |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_fail/T14350 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
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 | ^^^^^
Change History (4)
comment:1 Changed 10 months ago by
Description: | modified (diff) |
---|
comment:2 Changed 10 months ago by
Cc: | simonpj added |
---|
comment:3 Changed 10 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → typecheck/should_fail/T14350 |
Fixed by
In 74cd1be0/ghc: Don't deeply expand insolubles Trac #13450 went bananas if we expand insoluble constraints. Better just to leave them un-expanded. I'm not sure in detail about why it goes so badly wrong; but regardless, the less we mess around with insoluble contraints the better the error messages will be.
Sorry I mis-typed the trac ticket in the commit.
Note: See
TracTickets for help on using
tickets.
Commit f20cf982f126aea968ed6a482551550ffb6650cf (
Remove wc_insol from WantedConstraints
) introduced this regression.