Re: #14419: Check kinds for ambiguity

"GHC" <[email protected]>
Newsgroups gmane.comp.lang.haskell.glasgow.bugs
Message-ID <[email protected]>
#14419: Check kinds for ambiguity
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeInType,
                                     |  VisibleDependentQuantification
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * keywords:  TypeInType => TypeInType, VisibleDependentQuantification


Comment:

 Here is how to trigger the same issue using visible dependent
 quantification:

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 import Data.Kind

 type family F a
 data Ex (x :: forall a -> F a -> Type)
 }}}
 {{{
 GHCi, version 8.9.20190227: https://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:10:1: error:
     • Couldn't match type ‘F a’ with ‘F a0’
       Expected type: F a -> *
         Actual type: F a0 -> *
       NB: ‘F’ is a non-injective type family
       The type variable ‘a0’ is ambiguous
     • In the ambiguity check for the kind annotation on the type variable
 ‘x’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the data type declaration for ‘Ex’
    |
 10 | data Ex (x :: forall a -> F a -> Type)
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14419#comment:14>
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.