[GHC] #13006: Possible program should type check but does not using Implicit Parameters and Vectors

[GHC]

#13006: Possible program should type check but does not using Implicit Parameters
and Vectors
-------------------------------------+-------------------------------------
           Reporter:  clinton        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2-rc2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I think (but I'm not sure) that the following code should type check. This
 will require using the 'vector' package to illustrate this issue, sorry I
 couldn't create an example without it.

 Either uncommenting the explicit `m ()` signature or changing the type to
 the simpler `D m` data type will allow the code to compile.

 {{{
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE KindSignatures #-}

 import Data.Vector.Unboxed.Mutable (MVector)
 import Control.Monad.Primitive (PrimMonad, PrimState)

 data D (x :: * -> *)

 type T m = MVector (PrimState m) Int
 --type T m = D m

 h :: forall m. PrimMonad m => T m -> m ()
 h x = let f _ = (let ?v = x in g) {- :: m () -} in f undefined

 g :: (PrimMonad m , ?v :: T m) => m ()
 g = undefined

 main = pure ()
 }}}

 Alternatively, including `g` into the let binding as opposed to the top
 level will also compile:

 {{{
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE KindSignatures #-}

 import Data.Vector.Unboxed.Mutable (MVector)
 import Control.Monad.Primitive (PrimMonad, PrimState)

 data D (x :: * -> *)

 type T m = MVector (PrimState m) Int
 --type T m = D m

 h :: forall m. PrimMonad m => T m -> m ()
 h x =
   let
     f _ = (let ?v = x in g) {- :: m () -}
     g :: (PrimMonad m , ?v :: T m) => m ()
     g = undefined
   in f undefined

 main = pure ()
 }}}

 Perhaps this isn't a bug and has to do with the rank-2 type inside of
 Vector, but I'm just putting in this bug report to confirm.

 This is an issue as of 8.0.2-rc2.

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