[GHC] #10931: layers-0.1 does not compile with ghc-7.10 (likely a regression from ghc-7.8)

4 Oct 2015

      #10931: layers-0.1 does not compile with ghc-7.10 (likely a regression from
ghc-7.8)
-------------------------------------+-------------------------------------
           Reporter:  slyfox         |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           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):                 |
-------------------------------------+-------------------------------------
 Distilled example is the following:

 {{{#!hs
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE AllowAmbiguousTypes #-} -- not needed for 7.8, should not be
 needed for 7.10 as well

 {-# OPTIONS_GHC -Wall #-}

 module L () where

 import Prelude () -- clean up

 data IdT f a = IdC (f a)

 class ( m ~ Outer m (Inner m) ) => BugC (m :: * -> *) where
     type Inner m :: * -> *
     type Outer m :: (* -> *) -> * -> *

     bug :: ( forall n. ( n ~ Outer n (Inner n)
                        , Outer n ~ Outer m
                        )
             => Inner n a)
         -> m a

 instance BugC (IdT m) where
     type Inner (IdT m) = m
     type Outer (IdT m) = IdT

     bug f = IdC f
 }}}

 ghc-7.8 compiles the sample just fine:
 {{{
 $ ghci a.hs
 GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
 Loading package ghc-prim ... linking ... done.
 Loading package integer-gmp ... linking ... done.
 Loading package base ... linking ... done.
 [1 of 1] Compiling L                ( a.hs, interpreted )
 Ok, modules loaded: L.
 *L> :t bug
 bug
   :: (BugC (t1 t), Outer (t1 t) ~ t1, Inner (t1 t) ~ t) =>
      (forall (n :: * -> *).
       (n ~ Outer n (Inner n), Outer n ~ Outer (t1 t)) =>
       Inner n a)
      -> t1 t a

 }}}

 ghc-7.10 can't build it even with AllowAmbiguousTypes
 {{{
 $ ghci a.hs
 GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling L                ( a.hs, interpreted )

 a.hs:28:17:
     Couldn't match type ‘m’ with ‘Inner (IdT m)’
       ‘m’ is a rigid type variable bound by
           the instance declaration at a.hs:24:10
     Expected type: Outer (IdT m) (Inner (IdT m))
       Actual type: IdT m
     Relevant bindings include
       f :: forall (n :: * -> *).
            (n ~ Outer n (Inner n), Outer n ~ Outer (IdT m)) =>
            Inner n a
         (bound at a.hs:28:9)
       bug :: (forall (n :: * -> *).
               (n ~ Outer n (Inner n), Outer n ~ Outer (IdT m)) =>
               Inner n a)
              -> IdT m a
         (bound at a.hs:28:5)
     In the first argument of ‘IdC’, namely ‘f’
     In the expression: IdC f
     In an equation for ‘bug’: bug f = IdC f
 Failed, modules loaded: none.
 }}}

 Without AllowAmbiguousTypes the error gives a hint
 on ambiguity (which does not really exist as I understand associated type
 families):

 {{{
 $ ghci a-no-ambig-language.hs
 GHCi, version 7.10.2: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling L                ( a.hs, interpreted )

 a.hs:28:17:
     Couldn't match type ‘m’ with ‘Inner (IdT m)’
       ‘m’ is a rigid type variable bound by
           the instance declaration at a.hs:24:10
     Expected type: Outer (IdT m) (Inner (IdT m))
       Actual type: IdT m
     Relevant bindings include
       f :: forall (n :: * -> *).
            (n ~ Outer n (Inner n), Outer n ~ Outer (IdT m)) =>
            Inner n a
         (bound at a.hs:28:9)
       bug :: (forall (n :: * -> *).
               (n ~ Outer n (Inner n), Outer n ~ Outer (IdT m)) =>
               Inner n a)
              -> IdT m a
         (bound at a.hs:28:5)
     In the first argument of ‘IdC’, namely ‘f’
     In the expression: IdC f
     In an equation for ‘bug’: bug f = IdC f
 Failed, modules loaded: none.
 }}}

 It seems that ghc-7.8 is more correct here.

 Thanks!

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