[GHC] #11305: TC Regression

28 Dec 2015


      #11305: TC Regression
-------------------------------------+-------------------------------------
           Reporter:  hvr            |             Owner:
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.0.1
          Component:  Compiler       |           Version:  7.11
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 TODO: figure out better summary ;-)

 The following snippet extracted from Edward's `profunctors` package
 compiles with GHC 7.10.3, but fails to type-check with GHC HEAD:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeOperators #-}

 module Data.Profunctor.Strong where

 import Control.Arrow
 import Control.Category
 import Data.Tuple
 import Prelude hiding (id,(.))

 infixr 0 :->
 type p :-> q = forall a b. p a b -> q a b

 class Profunctor p where
   dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

 class ProfunctorFunctor t where
   promap    :: Profunctor p => (p :-> q) -> t p :-> t q

 class ProfunctorFunctor t => ProfunctorMonad t where
   proreturn :: Profunctor p => p       :-> t p
   projoin   :: Profunctor p => t (t p) :-> t p

 class ProfunctorFunctor t => ProfunctorComonad t where
   proextract   :: Profunctor p => t p :-> p
   produplicate :: Profunctor p => t p :-> t (t p)

 class Profunctor p => Strong p where
   first' :: p a b  -> p (a, c) (b, c)
   first' = dimap swap swap . second'

   second' :: p a b -> p (c, a) (c, b)
   second' = dimap swap swap . first'

 ----------------------------------------------------------------------------

 newtype Tambara p a b = Tambara { runTambara :: forall c. p (a, c) (b, c)
 }

 instance Profunctor p => Profunctor (Tambara p) where
   dimap f g (Tambara p) = Tambara $ dimap (first f) (first g) p

 instance ProfunctorFunctor Tambara where
   promap f (Tambara p) = Tambara (f p)

 instance ProfunctorComonad Tambara where
   proextract (Tambara p) = dimap (\a -> (a,())) fst p

   produplicate (Tambara p) = Tambara (Tambara $ dimap hither yon p)
     where
       hither :: ((a, b), c) -> (a, (b, c))
       hither ~(~(x,y),z) = (x,(y,z))

       yon    :: (a, (b, c)) -> ((a, b), c)
       yon    ~(x,~(y,z)) = ((x,y),z)

 instance Profunctor p => Strong (Tambara p) where
   first' = runTambara . produplicate
 }}}

 {{{
 Strong.hs:57:12: error:
     • Couldn't match type ‘Tambara p (a, c) (b, c)’ with ‘forall c1.
 Tambara p (a, c1) (b, c1)’
       Expected type: Tambara (Tambara p) a b -> Tambara p (a, c) (b, c)
         Actual type: Tambara (Tambara p) a b -> forall c. Tambara p (a, c)
 (b, c)
     • In the first argument of ‘(.)’, namely ‘runTambara’
       In the expression: runTambara . produplicate
       In an equation for ‘first'’: first' = runTambara . produplicate
     • Relevant bindings include first' :: Tambara p a b -> Tambara p (a,
 c) (b, c) (bound at Strong.hs:57:3)
 }}}

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