Changes between Initial Version and Version 1 of Ticket #7420


Ignore:
Timestamp:
Nov 16, 2012 8:47:52 AM (2 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