Created
June 28, 2021 09:10
-
-
Save guibou/2070c0c201e0ce3fb79549b99a6bfbf8 to your computer and use it in GitHub Desktop.
Deriving Via and RankNTypes constraints do not play well and leads to redundant constraints
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# OPTIONS -Wall -Wredundant-constraints #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE ConstrainedClassMethods #-} | |
| {-# LANGUAGE StandaloneDeriving #-} | |
| {-# LANGUAGE DerivingVia #-} | |
| {-# LANGUAGE UndecidableInstances #-} | |
| import Data.Coerce | |
| import Data.Constraint | |
| import Data.Reflection | |
| newtype New t = New t | |
| deriving (Show) | |
| class Foo a where | |
| localDef :: Needs a => a | |
| type Needs a :: Constraint | |
| instance Foo (New a) where | |
| localDef = New given | |
| type Needs (New a) = Given a | |
| data A = A | |
| -- Here I do have a "Redundant constraint" error | |
| -- Need.hs:29:1: warning: [-Wredundant-constraints] | |
| -- • Redundant constraint: Needs A | |
| -- • In an expression type signature: | |
| -- Needs A => A | |
| -- In the expression: | |
| -- coerce @(New A) @A (localDef @(New A)) :: Needs A => A | |
| -- In an equation for ‘localDef’: | |
| -- localDef = coerce @(New A) @A (localDef @(New A)) :: Needs A => A | |
| -- When typechecking the code for ‘localDef’ | |
| -- in a derived instance for ‘Foo A’: | |
| -- To see the code I am typechecking, use -ddump-deriv | |
| -- | | |
| -- 29 | deriving via (New A) instance Foo A | |
| -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | |
| deriving via (New A) instance Foo A | |
| -- If I try to write the code generated by deriving via (see the above error | |
| -- message), same error: | |
| -- Need.hs:35:11: warning: [-Wredundant-constraints] | |
| -- • Redundant constraint: Needs A | |
| -- • In an expression type signature: | |
| -- Needs A => A | |
| -- In the expression: | |
| -- coerce @(New A) @A (localDef @(New A)) :: Needs A => A | |
| -- In an equation for ‘dlocalDef’: | |
| -- dlocalDef = coerce @(New A) @A (localDef @(New A)) :: Needs A => A | |
| -- | | |
| -- 35 | Needs A => A | |
| -- | | |
| dlocalDef :: Needs A => A | |
| dlocalDef = coerce | |
| @(New A) @A | |
| (localDef @(New A)) :: | |
| Needs A => A | |
| -- Note that the version without `Needs A` here does indeed not generate an error: | |
| dlocalDef' :: Needs A => A | |
| dlocalDef' = coerce | |
| @(New A) @A | |
| (localDef @(New A)) :: | |
| A | |
| -- I don't really understand why: | |
| -- - There is a redundant constraint warning | |
| -- - Why removing the constraint in dlocalDef' is fine |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment