Ambiguous types in pattern synonym not determined by functional dependencies

The Glorious Glasgow Haskell Compilation System, version 8.1.20160117

{-# 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:

pattern Len xs <- UnOp (Un OpLen _) xs

but the inferred type is rejected:

-- >>> :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:

len :: GetTy a rep => E [a] -> E Int
len = UnOp (Un OpLen length)

but adding it to the pattern makes it fail:

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?

Trac metadata

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture