New subject: [GHC] #12531: Holes should be representation-polymorphic (was: Holes should be kind-polymorphic)

24 Aug 2016

      #12531: Holes should be kind-polymorphic
-------------------------------------+-------------------------------------
           Reporter:  mniip          |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Other
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I often use holes while writing long expressions out in GHCi in order to
 let the typechecker assist me with type inference.

 Sometimes though I find myself in a situation where I want to use holes
 near unlifted types and results in kind check messages obscuring the holes
 or having hole errors not show up at all:

 {{{#!hs
...
I# (_ +# 1#)
<interactive>:5:5: error:
     • Couldn't match a lifted type with an unlifted type
       When matching the kind of ‘Int#’
     • In the first argument of ‘(+#)’, namely ‘_’
       In the first argument of ‘I#’, namely ‘(_ +# 1#)’
       In the expression: I# (_ +# 1#)

 <interactive>:5:5: error:
     • Found hole: _ :: Int#
     • In the first argument of ‘(+#)’, namely ‘_’
       In the first argument of ‘I#’, namely ‘(_ +# 1#)’
       In the expression: I# (_ +# 1#)
     • Relevant bindings include it :: Int (bound at <interactive>:5:1)
 }}}

 (Don't be deceived, the type of `_` there is actually `Int# |> (TYPE
 U(hole:{a1qG}, 'IntRep, 'PtrRepLifted)_N)_N`)

 Perhaps the type of `_` should be `forall r (a :: TYPE r). a` or even
 `forall k (a :: k). a` instead?

 This might lead to issues with `-fdefer-typed-holes` but maybe we could at
 first disallow deferred unlifted-kinded holes? But in theory a hole is
 just a call to `error` which is representation-polymorphic already.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12531
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

[GHC] #12531: Holes should be kind-polymorphic

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)