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 |