## #15593 closed bug (duplicate)

# QuantifiedConstraints: trouble with type family

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.1 |

Component: | Compiler | Version: | 8.5 |

Keywords: | QuantifiedConstraints, ConstraintKinds | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | #14860 | Differential Rev(s): | |

Wiki Page: |

### Description

{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances #-} import Data.Kind data TreeF a b = T0 | T1 a | T2 b b -- from Data.Reify class MuRef (a :: Type) where type DeRef a :: Type -> Type class (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree

fails with

$ ~/code/qc-ghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 351.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 351.hs, interpreted ) 351.hs:12:10: error: • Couldn't match type ‘DeRef (tree xx)’ with ‘TreeF xx’ arising from the superclasses of an instance declaration • In the instance declaration for ‘MuRef1 tree’ | 12 | instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude>

What I want to write:

{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes #-} import Data.Kind -- from Data.Reify class MuRef (a :: Type) where type DeRef a :: Type -> Type type T = Type type TT = T -> T type TTT = T -> TT class (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT) instance (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx)) => MuRef1 (f :: TT) (deRef1 :: TT -> TTT)

where I am trying to capture MuRef1 & DeRef1

class MuRef1 (f :: TT) where type DeRef1 f :: TTT muRef1 :: proxy (f a) -> Dict (MuRef (f a), DeRef (f a) ~ DeRef1 f a)

Workarounds: I think splitting the class alias & quantification does the job (I haven't tested it but it compiles), I want to know if the first two programs are meant to compile or not

{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #-} -- .. class (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx instance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx class (forall xx. cls xx) => Forall cls instance (forall xx. cls xx) => Forall cls class Forall (MuRef1_ f deRef1) => MuRef1 f deRef1 instance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1

or as a regular type/constraint synonym (at the loss of partial application)

type MuRef1 f deRef1 = (forall xx. (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx))

### Change History (4)

### comment:2 Changed 13 months ago by

Oh dear can of worms, what about the workaround then: does that compile on HEAD? I will have to read that ticket

{-# Language KindSignatures, TypeFamilies, QuantifiedConstraints, FlexibleInstances, DataKinds, TypeInType, MultiParamTypeClasses, UndecidableInstances, AllowAmbiguousTypes, FlexibleContexts #-} import Data.Kind class MuRef (a :: Type) where type DeRef a :: Type -> Type class (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx instance (MuRef (f xx), DeRef (f xx) ~ deRef1 f xx) => MuRef1_ f deRef1 xx class (forall xx. cls xx) => Forall cls instance (forall xx. cls xx) => Forall cls class Forall (MuRef1_ f deRef1) => MuRef1 f deRef1 instance Forall (MuRef1_ f deRef1) => MuRef1 f deRef1

### comment:3 Changed 13 months ago by

The program you posted in comment:2 compiles in both GHC 8.6.1 and HEAD.

### comment:4 Changed 7 months ago by

Related Tickets: | → #14860 |
---|---|

Resolution: | → duplicate |

Status: | new → closed |

Update: GHC HEAD now *does* allow quantified constraints to be headed by `(~)`

. Unfortunately, the original example still won't compile due to the fact that the quantified constraint's head mentions a type family:

Bug.hs:11:1: error: • Illegal type synonym family application ‘DeRef (tree xx)’ in instance: DeRef (tree xx) ~ TreeF xx • In the quantified constraint ‘forall xx. DeRef (tree xx) ~ TreeF xx’ In the context: forall xx. DeRef (tree xx) ~ TreeF xx While checking the super-classes of class ‘MuRef1’ In the class declaration for ‘MuRef1’ | 11 | class (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:12:10: error: • Illegal type synonym family application ‘DeRef (tree xx)’ in instance: DeRef (tree xx) ~ TreeF xx • In the quantified constraint ‘forall xx. DeRef (tree xx) ~ TreeF xx’ In the instance declaration for ‘MuRef1 tree’ | 12 | instance (forall xx. DeRef (tree xx) ~ TreeF xx) => MuRef1 tree | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is the subject of #14860, so I'm going to close this ticket in favor of that one.

**Note:**See TracTickets for help on using tickets.

Unfortunately, this is not going to work, since you can't quantify over constraints that are headed by

`(~)`

. See #15359.GHC HEAD at least gives you a slightly more informative error message about this: