[GHC] #9607: Type checking regression between GHC 7.6 and 7.8

[GHC]

#9607: Type checking regression between GHC 7.6 and 7.8
-------------------------------------+-------------------------------------
       Reporter:  jstolarek          |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler (Type     |                 Version:  7.8.3
  checker)                           |        Operating System:
       Keywords:                     |  Unknown/Multiple
   Architecture:  Unknown/Multiple   |         Type of failure:  GHC
     Difficulty:  Unknown            |  rejects valid program
     Blocked By:                     |               Test Case:
Related Tickets:                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 Jason McCarty [http://www.haskell.org/pipermail/haskell-
 cafe/2014-September/116076.html reported on Haskell-cafe] that this code
 used to work with GHC 7.6 but in GHC 7.8 it requires
 `AllowAmbiguousTypes`:

 {{{#!hs
 -- The code below is simplified from code that computes a tensor product
 of
 -- a tensor with an identity matrix whose size is determined from the
 -- shapes of the input and output tensors.
 {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
 --{-# LANGUAGE AllowAmbiguousTypes #-}
 module Tensors where
 import GHC.TypeLits

 type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat]
 type instance '[] ++ bs = bs
 type instance (a ': as) ++ bs = a ': (as ++ bs)

 data Tensor (s :: [Nat]) = Tensor -- content elided

 -- apparently GHC reduces (++) enough to see that n is determined
 leftUnit :: Tensor s -> Tensor ('[n, n] ++ s)
 leftUnit Tensor = Tensor

 -- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes
 rightUnit :: Tensor s -> Tensor (s ++ '[n, n])
 rightUnit Tensor = Tensor

 -- also accepted without AllowAmbiguousTypes
 outsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n])
 outsideUnit Tensor = Tensor

 useleftUnit :: Tensor '[1,1,2]
 useleftUnit = leftUnit Tensor -- type of Tensor is inferred

 userightUnit :: Tensor '[1,2,2]
 userightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided
 }}}

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