#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by simonpj): One other thing. As I said in our call today, it's striking how narrow are the use-cases for a coercion-quantified type: * We can't ''declare'' a function with type `f :: (t1 ~# t2) => blah`, because currently `(t1 ~# t2)` is not a constraint (see Trac #15648) and is never implicitly instantiated. * We can't ''infer'' a function with type `f :: (t1 ~# t2) => blah`. And if we did, it wouldn't be instantiated implicitly. And so ''a fortiori'' we can't have coercion-quantified variants of such types. '''So the ''only'' functions that can have these coercion-quantified types are the workers of data constructors'''. Am I right? If so, can we say so explicitly on the wiki page? That seems like a lot of work for a narrow use-case! And yet, and yet... it's a very important case. Note also that we cannot write an exactly-equivalent type signature with GADT-syntax, because we don't have source-syntax of `t1 ~# t2`, let alone for `forall (co:t1~#t2). blah`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15497#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler