Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14799 closed bug (fixed)

QuantifiedConstraints: Problems with Typeable

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
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

This compiles

{-# Language GADTs, ConstraintKinds, ScopedTypeVariables, QuantifiedConstraints #-}

import Data.Typeable

data Ex cls where
  MkEx :: cls xx => xx -> Ex cls

a :: Ex Typeable -> TypeRep
a (MkEx (_::xx)) = typeRep @_ @xx Proxy

-- b :: (forall xx. cls xx => Typeable xx) => Ex cls -> TypeRep
-- b (MkEx (_::xx)) = typeRep @_ @xx Proxy

c :: (forall xx. cls xx => Show xx) => Ex cls -> String
c (MkEx xx) = show xx

but uncommenting b is too much:

$ qc hs/189-bug.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/189-bug.hs, interpreted )

hs/189-bug.hs:12:20: error:
    • Could not deduce (Typeable xx) arising from a use of ‘typeRep’
      from the context: forall xx. cls xx => Typeable xx
        bound by the type signature for:
                   b :: forall (cls :: * -> Constraint).
                        (forall xx. cls xx => Typeable xx) =>
                        Ex cls -> TypeRep
        at hs/189-bug.hs:11:1-60
      or from: cls xx
        bound by a pattern with constructor:
                   MkEx :: forall xx (cls :: * -> Constraint). cls xx => xx -> Ex cls,
                 in an equation for ‘b’
        at hs/189-bug.hs:12:4-15
    • In the expression: typeRep @_ @xx Proxy
      In an equation for ‘b’: b (MkEx (_ :: xx)) = typeRep @_ @xx Proxy
   |
12 | b (MkEx (_::xx)) = typeRep @_ @xx Proxy
   |                    ^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

This is maybe because of the Typeable solver.

Change History (4)

comment:1 Changed 19 months ago by Iceland_jack

It works by creating a class alias for Typeable

class Typeable a => Typeable' a where
  typeRep' :: proxy a -> TypeRep
  typeRep' proxy = typeRep proxy

instance Typeable a => Typeable' a

b :: (forall xx. cls xx => Typeable' xx) => Ex cls -> TypeRep
b (MkEx (_::xx)) = typeRep' @_ @xx Proxy

comment:2 Changed 19 months ago by RyanGlScott

So your first example didn't compile for me:

Bug.hs:9:31: error: parse error on input ‘@’
  |
9 | a (MkEx (_::xx)) = typeRep @_ @xx Proxy
  |                               ^

So I added TypeApplications:

{-# Language GADTs, ConstraintKinds, ScopedTypeVariables, QuantifiedConstraints #-}
{-# Language TypeApplications #-}

import Data.Typeable

data Ex cls where
  MkEx :: cls xx => xx -> Ex cls

a :: Ex Typeable -> TypeRep
a (MkEx (_::xx)) = typeRep @_ @xx Proxy

b :: (forall xx. cls xx => Typeable xx) => Ex cls -> TypeRep
b (MkEx (_::xx)) = typeRep @_ @xx Proxy

c :: (forall xx. cls xx => Show xx) => Ex cls -> String
c (MkEx xx) = show xx

And now it compiles! So I'm not sure what you're doing differently. (Please make sure you've given us all the language extensions/flags you're using—it makes a huge difference!)

comment:3 Changed 19 months ago by Iceland_jack

Resolution: fixed
Status: newclosed

Seems like Simon's latest patch fixed this

comment:4 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.