Re: [GHC] #5296: Add explicit type applications

I have two open design questions:
1. What to do with `:type` in GHCi? Suppose we have `pair :: forall a. a -> forall b. b -> (a,b)`. I ask `:type pair 3`. The real type of this expression is `forall b. b -> (a0, b)`, where `a0` is the type of the overloaded `3`. The problem is that this type loses the fact that we need `Num a0`. We could say `forall b. Num a0 => b -> (a0, b)`, which is a
#5296: Add explicit type applications -------------------------------------+------------------------------------- Reporter: dsf | Owner: goldfire Type: feature request | Status: new Priority: low | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.0.3 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: 1897 | Blocking: Related Tickets: #4466 | Differential Revisions: Phab:D1138 -------------------------------------+------------------------------------- Comment (by WrenThornton): Replying to [comment:17 goldfire]: little closer. Would we report that without `-fprint-explicit-foralls`? It would be wrong to say `forall a b. Num a => b -> (a, b)` (as is done today, even with this patch) because we can't instantiate `a` with a further visible type application. IMO, the type `forall a b. Num a => b -> (a, b)` is wrong for the expression `(pair 3)` aka `(pair @a (fromInteger @a $3))`, because the type `a` is fixed, albeit unknown. My first inclination would be to say those expressions have type `iota a. Num a => forall b. b -> (a, b)`. Of course, I wouldn't expect most folks to know anything about the `iota` quantifier, so I probably wouldn't print it that way. Do we have a notation for metavariables yet? We could say `Num ?a => forall b. b -> (?a, b)` supposing `?a` is the way we write a metavariable (rather than that syntax being used by ImplicitParams).
2. It would be nice to be able to say `3 @Int` instead of `(3 :: Int)`.
I agree with spj here. There's not really any benefit in terms of expressibility nor brevity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/5296#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC