#12677: Type equality in constraint not used? -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is a hard one to fix, surprisingly. The problem is that you've declared `a` to have type `k` and then used `a` as an argument to `->`. Of course, `->` expects a `Type`. So GHC should insert add a cast, forming `a |> η`, for the argument to `->`. The problem is that this would require using the equality proof for `Type ~ k` as the body of `η`, and the current type system simply does not allow this. [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unl... Here] are some notes on the matter, though they were not written to be digested by anyone but me. I don't expect this will be fixed until we have `-XDependentTypes`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12677#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler