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

#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

#11655: Ambiguous types in pattern synonym not determined by functional dependencies -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | PatternSynonyms, | FunctionalDependencies, GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * keywords: => PatternSynonyms, FunctionalDependencies, GADTs * cc: mpickering (added) * component: Compiler => Compiler (Type checker) Comment: Inferred type is still rejected in 8.1.20160503. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11655#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC