Opened 18 months ago

Last modified 16 months 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 16 months ago by thomie

Cc: mpickering added
Component: CompilerCompiler (Type checker)
Keywords: PatternSynonyms FunctionalDependencies GADTs added

Inferred type is still rejected in 8.1.20160503.

Note: See TracTickets for help on using tickets.