Opened 2 years ago
Last modified 2 years ago
#11655 new bug
Ambiguous types in pattern synonym not determined by functional dependencies
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.1 |
Keywords: | PatternSynonyms, FunctionalDependencies, GADTs | Cc: | mpickering |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
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?
Change History (1)
comment:1 Changed 2 years ago by
Cc: | mpickering added |
---|---|
Component: | Compiler → Compiler (Type checker) |
Keywords: | PatternSynonyms FunctionalDependencies GADTs added |
Note: See
TracTickets for help on using
tickets.
Inferred type is still rejected in 8.1.20160503.