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

24 Aug 2016


      #12531: Holes should be kind-polymorphic
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                Owner:
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Other             |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by mniip:

@@ -5,2 +5,2 @@
- near unlifted types and results in kind check messages obscuring the holes
- or having hole errors not show up at all:
+ near unlifted types and that results in kind check messages obscuring the
+ holes or having hole errors not show up at all:

New description:

 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 that 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#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

    