#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