[GHC] #14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N)

[GHC]

#14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:  duplicate         |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12677            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => closed
 * resolution:   => duplicate
 * related:   => #12677


Comment:

 Yes indeed. Here is a simpler version of the issue you've encountered:

 {{{#!hs
 {-# LANGUAGE DataKinds, GADTs, PolyKinds, ScopedTypeVariables #-}

 import Data.Proxy

 data N = O | S N

 data Foo (a :: k) where
   MkFoo :: forall (a :: k). N ~ k => Proxy (a :: N) -> Foo a
 }}}

 Here, GHC complains:

 {{{
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 Bug.hs:8:45: error:
     • Expected kind ‘N’, but ‘a1’ has kind ‘k1’
     • In the first argument of ‘Proxy’, namely ‘(a :: N)’
       In the type ‘Proxy (a :: N)’
       In the definition of data constructor ‘MkFoo’
   |
 8 |   MkFoo :: forall (a :: k). N ~ k => Proxy (a :: N) -> Foo a
   |                                             ^
 }}}

 Despite the fact that GHC is supposed to know that `N ~ k`. Alas, this is
 due to an unfortunate limitation in how GHC's type system works. I'll
 quote Richard's comment
 [https://ghc.haskell.org/trac/ghc/ticket/12677#comment:2 here]:

 > This is a hard one to fix, surprisingly. The problem is that you've
 declared `a` to have type `k` and then used `a` as an argument to `->`. Of
 course, `->` expects a `Type`. So GHC should insert add a cast, forming `a
 |> η`, for the argument to `->`. The problem is that this would require
 using the equality proof for `Type ~ k` as the body of `η`, and the
 current type system simply does not allow this.
 [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality
 ​Here] are some notes on the matter, though they were not written to be
 digested by anyone but me.
 >
 > I don't expect this will be fixed until we have `-XDependentTypes`.

 **tl;dr** GHC's type system probably won't be smart enough to figure this
 out until dependent types are added. See #12677 for details.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14499#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler