#11387: Typecasting using type application syntax -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11350 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: It would make sense to do something a bit like this. If `a :: *` is a type, then a `Typeable a` constraint is essentially an (invisible) singleton witness to `a`; the visible singleton is `TypeRep a`. I think the Right Thing to do would be to get rid of the singleton construction and add pi-types, so that we have {{{#!hs doubleWhenInt :: pi a . a -> a doubleWhenInt @Int n = n + n doubleWhenInt @_ x = x }}} The `pi a .` quantifier corresponds to `forall a . Typeable a =>`. The type argument is operationally relevant, can be pattern-matched and hence is non-parametric. The argument would be invisible-by-default (e.g. you might write `doubleWhenInt True` at a call site) but could be made visible like other type arguments (e.g. `doubleWhenInt @Int 42` should be allowed). (It's not completely obvious whether arguments to pi-quantified functions should be in the type namespace or the term namespace, because they exist at both levels.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11387#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler