[GHC] #15122: Compiling a library problem with a local 8.5 build
#15122: Compiling a library problem with a local 8.5 build -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Keywords: | Operating System: MacOS X Architecture: x86_64 | Type of failure: GHC rejects (amd64) | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I’ve discovered that one library throws type checking exception when I try to compile it with my version of ghc compiler (I build it using `cabal new-build --with-compiler=/usr/local/bin/ghc-8.5.20180504`, the compiler was built from the master with 56974323ed427988059b5153bb43c694358cbb9b as the last commit), but it builds with 8.4.2 compiler (cabal new-build --with-compiler=/usr/local/bin/ghc-8.4.2). It’s really strange, so I tried to `make` the local version of 8.4.2 in the branch ghc-8.4.2-release, and found out that it cannot be built because there are missing some files that are necessary for build. So maybe I’m doing something wrong? And can it be that this library doesn’t type check with 8.5 because it’s built from source files? The exception can be seen here: https://gist.github.com/fmixing/93d140dc7dbe25199af28616c6a143da -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: Compiling a library problem with a local 8.5 build -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by fmixing: Old description:
I’ve discovered that one library throws type checking exception when I try to compile it with my version of ghc compiler (I build it using `cabal new-build --with-compiler=/usr/local/bin/ghc-8.5.20180504`, the compiler was built from the master with 56974323ed427988059b5153bb43c694358cbb9b as the last commit), but it builds with 8.4.2 compiler (cabal new-build --with- compiler=/usr/local/bin/ghc-8.4.2). It’s really strange, so I tried to `make` the local version of 8.4.2 in the branch ghc-8.4.2-release, and found out that it cannot be built because there are missing some files that are necessary for build. So maybe I’m doing something wrong? And can it be that this library doesn’t type check with 8.5 because it’s built from source files?
The exception can be seen here: https://gist.github.com/fmixing/93d140dc7dbe25199af28616c6a143da
New description: I’ve discovered that one library throws type checking exception when I try to compile it with my version of ghc compiler (I build it using `cabal new-build --with-compiler=/usr/local/bin/ghc-8.5.20180504`, the compiler was built from the master with 56974323ed427988059b5153bb43c694358cbb9b as the last commit), but it builds with 8.4.2 compiler (`cabal new-build --with-compiler=/usr/local/bin/ghc-8.4.2`). It’s really strange, so I tried to `make` the local version of 8.4.2 in the branch ghc-8.4.2-release, and found out that it cannot be built because there are missing some files that are necessary for build. So maybe I’m doing something wrong? And can it be that this library doesn’t type check with 8.5 because it’s built from source files? The exception can be seen here: https://gist.github.com/fmixing/93d140dc7dbe25199af28616c6a143da -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: Compiling a library problem with a local 8.5 build -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by mpickering): You may have found a bug but it's impossible to say without knowing what you are trying to compile. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: Compiling a library problem with a local 8.5 build -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: Operating System: MacOS X | Architecture: x86_64 Type of failure: GHC rejects | (amd64) valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by fmixing): Replying to [comment:2 mpickering]:
You may have found a bug but it's impossible to say without knowing what you are trying to compile.
type-level-sets library from https://github.com/dorchard/type-level-sets. It cannot be installed by `cabal install` because it is lacking of `TypeInType` extension in `Data.Type.Set`, so I downloaded it, added extension, imported `import GHC.Types`, `*` replaced with `GHC.Types.*`. So the current `Data.Type.Set` looks like https://gist.github.com/fmixing/695d46c6c5cc97398c3c44e05f23d764 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression involving overlapping instances -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * priority: normal => highest * os: MacOS X => Unknown/Multiple * component: Compiler => Compiler (Type checker) * architecture: x86_64 (amd64) => Unknown/Multiple Comment: Here is a slightly more minimal example: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where data Proxy (p :: k) = Proxy data Set (n :: [k]) where Empty :: Set '[] Ext :: e -> Set s -> Set (e ': s) type family (m :: [k]) :\ (x :: k) :: [k] where '[] :\ x = '[] (x ': xs) :\ x = xs (y ': xs) :\ x = y ': (xs :\ x) class Remove s t where remove :: Set s -> Proxy t -> Set (s :\ t) instance Remove '[] t where remove Empty Proxy = Empty instance {-# OVERLAPS #-} Remove (x ': xs) x where remove (Ext _ xs) Proxy = xs instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) => Remove (y ': xs) x where remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) }}} In GHC 8.4.2, this typechecks, but in GHC HEAD, it fails with: {{{ $ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:31:33: error: • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x)) from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) bound by the instance declaration at Bug.hs:(29,31)-(30,27) or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*])) bound by a pattern with constructor: Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s), in an equation for ‘remove’ at Bug.hs:31:11-18 Expected type: Set ((y : xs) :\ x) Actual type: Set (e : (s :\ x)) • In the expression: Ext y (remove xs x) In an equation for ‘remove’: remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) In the instance declaration for ‘Remove (y : xs) x’ • Relevant bindings include x :: Proxy x (bound at Bug.hs:31:22) xs :: Set s (bound at Bug.hs:31:17) y :: e (bound at Bug.hs:31:15) remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x) (bound at Bug.hs:31:3) | 31 | remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) | ^^^^^^^^^^^^^^^^^^^ }}} I'm unclear on what the exact culprit is here, so feel free to change the title further if overlapping instances turn out not to be the problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression involving overlapping instances -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression involving overlapping instances -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by RyanGlScott: Old description:
I’ve discovered that one library throws type checking exception when I try to compile it with my version of ghc compiler (I build it using `cabal new-build --with-compiler=/usr/local/bin/ghc-8.5.20180504`, the compiler was built from the master with 56974323ed427988059b5153bb43c694358cbb9b as the last commit), but it builds with 8.4.2 compiler (`cabal new-build --with- compiler=/usr/local/bin/ghc-8.4.2`). It’s really strange, so I tried to `make` the local version of 8.4.2 in the branch ghc-8.4.2-release, and found out that it cannot be built because there are missing some files that are necessary for build. So maybe I’m doing something wrong? And can it be that this library doesn’t type check with 8.5 because it’s built from source files?
The exception can be seen here: https://gist.github.com/fmixing/93d140dc7dbe25199af28616c6a143da
New description: This code, distilled from the `type-level-sets` library: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where data Proxy (p :: k) = Proxy data Set (n :: [k]) where Empty :: Set '[] Ext :: e -> Set s -> Set (e ': s) type family (m :: [k]) :\ (x :: k) :: [k] where '[] :\ x = '[] (x ': xs) :\ x = xs (y ': xs) :\ x = y ': (xs :\ x) class Remove s t where remove :: Set s -> Proxy t -> Set (s :\ t) instance Remove '[] t where remove Empty Proxy = Empty instance {-# OVERLAPS #-} Remove (x ': xs) x where remove (Ext _ xs) Proxy = xs instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) => Remove (y ': xs) x where remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) }}} Typechecks in GHC 8.4.2, but not in GHC HEAD: {{{ $ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:31:33: error: • Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x)) from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x) bound by the instance declaration at Bug.hs:(29,31)-(30,27) or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*])) bound by a pattern with constructor: Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s), in an equation for ‘remove’ at Bug.hs:31:11-18 Expected type: Set ((y : xs) :\ x) Actual type: Set (e : (s :\ x)) • In the expression: Ext y (remove xs x) In an equation for ‘remove’: remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) In the instance declaration for ‘Remove (y : xs) x’ • Relevant bindings include x :: Proxy x (bound at Bug.hs:31:22) xs :: Set s (bound at Bug.hs:31:17) y :: e (bound at Bug.hs:31:15) remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x) (bound at Bug.hs:31:3) | 31 | remove (Ext y xs) (x@Proxy) = Ext y (remove xs x) | ^^^^^^^^^^^^^^^^^^^ }}} This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.). -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeInType Comment: Never mind, I don't think this has anything to do with overlapping instances (or even type classes in particular), since the following also typechecks on GHC 8.4 but not on HEAD: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Proxy data Set (n :: [k]) where Empty :: Set '[] Ext :: e -> Set s -> Set (e ': s) type family (m :: [k]) :\ (x :: k) :: [k] where '[] :\ x = '[] (x ': xs) :\ x = xs (y ': xs) :\ x = y ': (xs :\ x) remove :: forall x y xs. ((y : xs) :\ x) ~ (y : (xs :\ x)) => Set (y ': xs) -> Proxy x -> Set ((y ': xs) :\ x) remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs)) remove' :: Set s -> Proxy x -> Proxy xs -> Set (xs :\ x) remove' = undefined }}} Here's the error message on HEAD if you compile with `-fprint-explicit- kinds`: {{{ $ /opt/ghc/head/bin/ghc -fprint-explicit-kinds Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:24:23: error: • Could not deduce: ((:\) * ((':) * e s) x :: [*]) ~~ ((':) * e ((:\) * s x) :: [*]) from the context: (:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs x) bound by the type signature for: remove :: forall k (x :: k) (y :: k) (xs :: [k]). ((:\) k ((':) k y xs) x ~ (':) k y ((:\) k xs x)) => Set k ((':) k y xs) -> Proxy k x -> Set k ((:\) k ((':) k y xs) x) at Bug.hs:(21,1)-(23,58) or from: ((k :: *) ~~ (* :: *), ((':) k y xs :: [k]) ~~ ((':) * e s :: [*])) bound by a pattern with constructor: Ext :: forall e (s :: [*]). e -> Set * s -> Set * ((':) * e s), in an equation for ‘remove’ at Bug.hs:24:9-16 Expected type: Set k ((:\) k ((':) k y xs) x) Actual type: Set * ((':) * e ((:\) * s x)) • In the expression: Ext y (remove' xs x (Proxy :: Proxy xs)) In an equation for ‘remove’: remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs)) • Relevant bindings include x :: Proxy k x (bound at Bug.hs:24:19) xs :: Set * s (bound at Bug.hs:24:15) y :: e (bound at Bug.hs:24:13) remove :: Set k ((':) k y xs) -> Proxy k x -> Set k ((:\) k ((':) k y xs) x) (bound at Bug.hs:24:1) | 24 | remove (Ext y xs) x = Ext y (remove' xs x (Proxy :: Proxy xs)) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK, even smaller now: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy data IsStar (a :: k) where IsStar :: IsStar (a :: *) type family F (a :: k) :: k foo :: (F a ~ F b) => IsStar a -> Proxy b -> Proxy (F a) -> Proxy (F b) foo IsStar _ p = p }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I see this and will take a stab when I can. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I took a look. Not yet complete but may help Richard. Analysing the program in cmmment:8. {{{ foo :: (F a ~ F b) => IsStar a -> Proxy b -> Proxy (F a) -> Proxy (F b) foo IsStar _ p = p }}} Informally we have {{{ (a::k), (b::k) [G] F a ~ F b [G] k ~ * [W] F a ~ F b }}} The given `k ~ *` should rewrite both the given and wanted equality, which should allow us to prove it no problem. The firsts slightly surprising thing is that the data constructor `IsStar` binds an existential: {{{ IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => IsStar @k a }}} Is this rigth? Well, if `IsStar` had some arguments it mmight be more persuasive {{{ data IsStar2 (a :: k) where IsStar2 :: a2 -> IsStar a2 }}} Now {{{ IsStar : forall k (a::k). forall (a2::*). (k~*, a~a2) => a2 -> IsStar @k a }}} We can't have `a` on the LHS of the arrow, because it has the wrong kind. Here's the implication we can't solve {{{ Implic { TcLevel = 2 Skolems = k_a1hM[sk:2] (a_a1hN[sk:2] :: k_a1hM[sk:2]) (b_a1hO[sk:2] :: k_a1hM[sk:2]) No-eqs = False Status = Unsolved Given = $d~_a1hQ :: (F a_a1hN[sk:2] :: k_a1hM[sk:2]) ~ (F b_a1hO[sk:2] :: k_a1hM[sk:2]) Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = a_a1hR[ssk:3] No-eqs = False Status = Unsolved Given = co_a1hS :: (k_a1hM[sk:2] :: *) ~# (* :: *) co_a1hT :: (a_a1hN[sk:2] :: k_a1hM[sk:2]) ~# (a_a1hR[ssk:3] :: *) Wanted = WC {wc_simple = [WD] hole{co_a1ig} {3}:: (F (b_a1hO[sk:2] |> co_a1hS) :: *) ~# (F a_a1hR[ssk:3] :: *) (CNonCanonical)} Binds = EvBindsVar<a1hV> a pattern with constructor: IsStar :: forall a. IsStar a, in an equation for `foo_a1hP' }} }}} Not yet sure why we can't solve it. At the crucial moment in typechecking `foo` we see this: {{{ work item = [WD] hole{co_a1hU} {0}:: (F a_a1hN[sk:2] :: k_a1hM[sk:2]) ~# (F b_a1hO[sk:2] :: k_a1hM[sk:2]) (CNonCanonical) inerts = {Equalities: [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *) ~# (* :: *) (CTyEqCan) [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] :: k_a1hM[sk:2]) ~# (fsk_a1i2[fsk:0] :: k_a1hM[sk:2]) (CTyEqCan) [G] co_a1i9 {1}:: (a_a1hN[sk:2] :: k_a1hM[sk:2]) ~# ((a_a1hR[ssk:3] |> Sym co_a1hS) :: k_a1hM[sk:2]) (CTyEqCan) Type-function equalities = [G] co_a1ib {0}:: (F (b_a1hO[sk:2] |> co_a1hS) :: *) ~# (fsk_a1ia[fsk:0] :: *) (CFunEqCan) [G] co_a1id {0}:: (F a_a1hR[ssk:3] :: *) ~# (fsk_a1ic[fsk:0] :: *) (CFunEqCan) Dictionaries = [G] $d~~_a1i8 {0}:: ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) ~~ ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) (CDictCan) [G] $d~_a1i7 {0}:: ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) ~ ((fsk_a1i2[fsk:0] |> co_a1hS) :: *) (CDictCan) }}} Note these two lines: {{{ [G] co_a1hS {0}:: (k_a1hM[sk:2] :: *) ~# (* :: *) (CTyEqCan) [G] co_a1i4 {1}:: (fsk_a1i0[fsk:0] :: k_a1hM[sk:2]) ~# (fsk_a1i2[fsk:0] :: k_a1hM[sk:2]) (CTyEqCan) }}} The first can rewrite the second, but we have not made it do so. I think because the substitution does not claim to be idempotent. But then we end up trying to prove that {{{ [W] fsk1 :: * ~ fsk2 : * }}{ and we have somehow lost the connection to our 'givens'. That's as far as I got. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15122: GHC HEAD typechecker regression
-------------------------------------+-------------------------------------
Reporter: fmixing | Owner: (none)
Type: bug | Status: new
Priority: highest | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: GHC rejects | Unknown/Multiple
valid program | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15122: GHC HEAD typechecker regression -------------------------------------+------------------------------------- Reporter: fmixing | Owner: (none) Type: bug | Status: closed Priority: highest | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: indexed- valid program | types/should_compile/T15122 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T15122 * resolution: => fixed Comment: Richard, I think you might enjoy the fix here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15122#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC