[GHC] #11655: Ambiguous types in pattern synonym not determined by functional dependencies

[GHC]

#11655: Ambiguous types in pattern synonym not determined by functional
dependencies
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           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:
-------------------------------------+-------------------------------------
 The Glorious Glasgow Haskell Compilation System, version 8.1.20160117

 {{{#!hs
 {-# LANGUAGE UndecidableInstances, KindSignatures, DataKinds, GADTs,
 MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances #-}

 data Ty ty where
   I  :: Ty Int
   A  :: Ty a -> Ty [a]

 data NUM    = MKINT
 data SCALAR = MKNUM NUM
 data TYPE   = MKSCALAR SCALAR  | MKARR TYPE

 -- Each type determines a TYPE
 --   Int   -> MKSCALAR (MKNUM MKINT)
 --   [Int] -> MKARR (MKSCALAR (MKNUM MKINT))
 class GetTy ty (rep :: TYPE) | ty -> rep where
   getTy :: Ty ty

 instance GetTy Int (MKSCALAR (MKNUM MKINT)) where
   getTy = I

 instance GetTy a rep => GetTy [a] (MKARR rep) where
   getTy = A getTy

 data Unary a b where
   Un :: (GetTy a a_rep, GetTy b b_rep) => UnOp a b -> (a -> b) -> Unary a
 b

 data UnOp a b where
   OpLen :: UnOp [a] Int

 data E a where
     UnOp :: Unary a b -> (E a -> E b)
 }}}

 Now I'd like to create an explicitly-bidirectional pattern synonym,
 defining a unidirectional pattern synonym works fine:

 {{{#!hs
 pattern Len xs <- UnOp (Un OpLen _) xs
 }}}

 but the inferred type is rejected:

 {{{#!hs
 -- >>> :i Len
 -- pattern Len :: () => (GetTy a a_rep, GetTy t b_rep,
 --                       a GHC.Prim.~# [a1], t GHC.Prim.~# Int) => E a ->
 E t
 pattern Len :: () => (GetTy a a_rep, GetTy t b_rep, a ~ [a1], t ~ Int) =>
 E a -> E t
 pattern Len xs <- UnOp (Un OpLen _) xs

 -- tgxg.hs:31:37-38: error: …
 --     • Could not deduce (GetTy a1 rep) arising from a pattern
 --       from the context: (GetTy a a_rep, GetTy t b_rep)
 --         bound by a pattern with constructor:
 --                    Un :: forall a b (a_rep :: TYPE) (b_rep :: TYPE).
 --                          (GetTy a a_rep, GetTy b b_rep) =>
 --                          UnOp a b -> (a -> b) -> Unary a b,
 --                  in a pattern synonym declaration
 --         at /tmp/tgxg.hs:31:25-34
 --       or from: (a ~ [a1], t ~ Int)
 --         bound by a pattern with constructor:
 --                    OpLen :: forall a. UnOp [a] Int,
 --                  in a pattern synonym declaration
 --         at /tmp/tgxg.hs:31:28-32
 --       The type variable ‘rep’ is ambiguous
 --     • In the declaration for pattern synonym ‘Len’
 -- Compilation failed.
 }}}

 Constructing it works fine:

 {{{#!hs
 len :: GetTy a rep => E [a] -> E Int
 len = UnOp (Un OpLen length)
 }}}

 but adding it to the pattern makes it fail:

 {{{#!hs
 pattern Len xs <- UnOp (Un OpLen _) xs where
         Len xs = len xs

 -- tgxg.hs:32:18-23: error: …
 --     • Could not deduce (GetTy a1 rep) arising from a use of ‘len’
 --       from the context: (GetTy a a_rep, GetTy t b_rep, a ~ [a1], t ~
 Int)
 --         bound by the type signature for:
 --                    Main.$bLen :: (GetTy a a_rep, GetTy t b_rep, a ~
 [a1], t ~ Int) =>
 --                                  E a -> E t
 --         at /tmp/tgxg.hs:(31,1)-(32,23)
 --       The type variable ‘rep’ is ambiguous
 --       These potential instances exist:
 --         instance GetTy Int ('MKSCALAR ('MKNUM 'MKINT))
 --           -- Defined at /tmp/tgxg.hs:14:10
 --         instance GetTy a rep => GetTy [a] ('MKARR rep)
 --           -- Defined at /tmp/tgxg.hs:17:10
 --     • In the expression: len xs
 --       In an equation for ‘$bLen’: $bLen xs = len xs
 -- Compilation failed.
 }}}

 Mixing functional dependencies, GADTs and pattern synonyms is confusing to
 me but is GHC correct that this type is ambiguous and if so what is
 missing?

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