Changes between Initial Version and Version 1 of Ticket #7420


Ignore:
Timestamp:
Nov 16, 2012 8:47:52 AM (3 years ago)
Author:
simonpj
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #7420

    • Property Difficulty changed from to Unknown
  • Ticket #7420 – Description

    initial v1  
    11The following simple code
    2 
     2{{{
    33{-# LANGUAGE DataKinds #-}[[BR]]
    44{-# LANGUAGE KindSignatures #-}[[BR]]
     
    1111
    1212hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))
    13 
    14 fails to type-check. The error message betrays a deep confusion in the
    15 kind checker:
    16 
     13}}}
     14fails to type-check. The error message betrays a deep confusion in the kind checker:
     15{{{
    1716/tmp/s3.hs:9:52:
    1817    Kind mis-match
    19 
    2018    An enclosing kind signature specified kind `Bool',
    21 
    2219    but `n' has kind `l'
    23 
    2420    In an expression type signature: Proxy (n :: Bool)
    25 
    2621    In the first argument of `undefined', namely
    2722      `(undefined :: Proxy (n :: Bool))'
    28 
    2923    In the expression: undefined (undefined :: Proxy (n :: Bool))
    30 
     24}}}
    3125If I write
    32 
     26{{{
    3327hUpdateAtLabel :: forall (l :: *) (n::Bool) v. v -> () -> ()
    34 
    3528hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))
    36 
     29}}}
    3730the code type-checks. However,
    38 
     31{{{
    3932hUpdateAtLabel :: forall l1 (l :: *) (n::Bool) v. v -> () -> ()
    40 
    4133hUpdateAtLabel _ () = undefined (undefined::Proxy (n::Bool))
    42 
     34}}}
    4335reports an error
    44 
     36{{{
    4537    Kind mis-match
    46 
    4738    An enclosing kind signature specified kind `Bool',
    48 
    4939    but `n' has kind `*'
    50 
     40}}}
    5141It looks like an off-by-one error, at least in the error message.
    5242