Should these extensions work together? I wasn't able to come up with a good motivating example; I was playing around with lenses, and thought a more restrictive class definition might aid type inference, though it turned out in that particular case it didn't. In the general case I think it might still be useful.

I didn't see any discussion on this, and it seemed like maybe it's an oversight.

Trac field | Value |
---|---|

Version | 8.0.1 |

Type | FeatureRequest |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

GHC can derive Functor for Okay, but rejects the equivalent Bad.

```
{-# LANGUAGE DeriveFunctor #-}
data Okay f g a b = Inl (f a b) | Inr (g a b) deriving (Functor)
newtype Bad f g a b = Bad (Either (f a b) (g a b)) deriving (Functor)
```

```
Can't make a derived instance of ‘Functor (Bad f g a)’:
Constructor ‘Bad’ must use the type variable only as the last argument of a data type
In the data declaration for ‘Bad’
```

Looking at this further, it seems like any type error in the file triggers the issue in the presence of triggersLoop.

Just to be clear, function definitions with the wrong arity still needed `triggersLoop (Q _ _) (Q _ _) = undefined`

to trigger the issue.

The layout rules for MultiWayIf currently require any lines starting with a comma to be further indented than the lines starting with a pipe when used in conjunction with PatternGuards. This is inconsistent with the examples given in https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/syntax-extns.html#pattern-guards. For instance, we can't use the same indentation in the second example as in the first without triggering a parser error.

```
{-# LANGUAGE PatternGuards, MultiWayIf #-}
fine a pred
| Just x <- a
, pred x = True
| otherwise = False
notFine a pred =
if | Just x <- a
, pred x -> True
| otherwise -> False
```

Though the documentation isn't *incorrect*, if this intentional it could be pointed out, since it's counterintuitive. Otherwise, if there's no reason for MulitWayIf to require further indentation that should be fixed.

The following incorrect arity triggers an infinite loop at compile time. The issue is somehow related to the use of (<=) in constraints of the Q data constructor; if I remove either of the constraints or add an (a <= c) constraint it works as you would expect.

```
{-# LANGUAGE GADTs, ExplicitNamespaces, TypeOperators, DataKinds #-}
import GHC.TypeLits (Nat, type (<=))
data Q a where
Q :: (a <= b, b <= c) => proxy a -> proxy b -> Q c
triggersLoop :: Q b -> Q b -> Bool
triggersLoop (Q _ _) (Q _ _) = print 'x' 'y'
```

Incorrect function definitions, like `foo :: a -> a ; foo _ x = x`

also result in an infinite loop.

I found #10742 (closed), which appears to be the same thing and is fixed in HEAD, so I'm closing

Trac field | Value |
---|---|

Resolution | Unresolved → ResolvedFixed |

I don't know if the summary I provided is what's really going on here, but I'm a little baffled why this doesn't typecheck. I can't see what injectivity has to do with it, since we're not trying to deduce that the arguments are the same from the result of an application being the same; rather we're doing the opposite. I've encountered plenty of obvious arithmetic laws that I've needed to unsafeCoerceConstraint away with doing type level arithmetic, but this seems like it should be trivial regardless.

```
{-# LANGUAGE GADTs, ExplicitNamespaces, TypeOperators, DataKinds #-}
{-# LANGUAGE ConstraintKinds, KindSignatures, PatternGuards #-}
import Data.Type.Equality ((:~:)(..))
import GHC.TypeLits (Nat, type (<=), type (-), type (+), type (<=?))
data SNat :: Nat -> * where
SSucc :: SNat a -> SNat (a + 1)
SZero :: SNat 0
heqHet :: SNat a -> SNat b -> Maybe (a :~: b)
heqHet SZero SZero = Just Refl
heqHet (SSucc a) (SSucc b)
| Just Refl <- heqHet a b = Just Refl
heqHet _ _ = Nothing
data Slice :: Nat -> Nat -> * where
Slice :: ((start + 1) <= end, end <= numElements)
=> SNat numElements -> SNat start -> SNat end
-> Slice numElements (end - start)
heqHet' :: Slice a b -> Slice a b' -> Bool
heqHet' (Slice _ start end) (Slice _ start' end')
| Just _ <- heqHet start start'
, Just _ <- heqHet end end' = True
| otherwise = False
```

```
Slice.hs:24:10:
Could not deduce (((start + 1) <=? a) ~ ((start + 1) <=? a))
from the context (b ~ (end - start), (start + 1) <= end, end <= a)
bound by a pattern with constructor
Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
((start + 1) <= end, end <= numElements) =>
SNat numElements
-> SNat start -> SNat end -> Slice numElements (end - start),
in an equation for ‘heqHet'’
at Slice.hs:24:10-26
or from (b' ~ (end1 - start1), (start1 + 1) <= end1, end1 <= a)
bound by a pattern with constructor
Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
((start + 1) <= end, end <= numElements) =>
SNat numElements
-> SNat start -> SNat end -> Slice numElements (end - start),
in an equation for ‘heqHet'’
at Slice.hs:24:30-48
NB: ‘GHC.TypeLits.<=?’ is a type function, and may not be injective
Relevant bindings include
heqHet' :: Slice a b -> Slice a b' -> Bool (bound at Slice.hs:24:1)
In the pattern: Slice _ start end
In an equation for ‘heqHet'’:
heqHet' (Slice _ start end) (Slice _ start' end')
| Just _ <- heqHet start start', Just _ <- heqHet end end' = True
| otherwise = False
Failed, modules loaded: none.
```

Trac field | Value |
---|---|

Version | 7.10.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

I don't know if the summary I provided is what's really going on here, but I'm a little baffled why this doesn't typecheck. I can't see what injectivity has to do with it, since we're not trying to deduce that the arguments are the same from the result of an application being the same; rather we're doing the opposite. I've encountered plenty of obvious arithmetic laws that I've needed to unsafeCoerceConstraint away with doing type level arithmetic, but this seems like it should be trivial regardless.

```
{-# LANGUAGE GADTs, ExplicitNamespaces, TypeOperators, DataKinds #-}
{-# LANGUAGE ConstraintKinds, KindSignatures, PatternGuards #-}
import Data.Type.Equality ((:~:)(..))
import GHC.TypeLits (Nat, type (<=), type (-), type (+), type (<=?))
data SNat :: Nat -> * where
SSucc :: SNat a -> SNat (a + 1)
SZero :: SNat 0
heqHet :: SNat a -> SNat b -> Maybe (a :~: b)
heqHet SZero SZero = Just Refl
heqHet (SSucc a) (SSucc b)
| Just Refl <- heqHet a b = Just Refl
heqHet _ _ = Nothing
data Slice :: Nat -> Nat -> * where
Slice :: ((start + 1) <= end, end <= numElements)
=> SNat numElements -> SNat start -> SNat end
-> Slice numElements (end - start)
heqHet' :: Slice a b -> Slice a b' -> Bool
heqHet' (Slice _ start end) (Slice _ start' end')
| Just _ <- heqHet start start'
, Just _ <- heqHet end end' = True
| otherwise = False
```

```
Slice.hs:24:10:
Could not deduce (((start + 1) <=? a) ~ ((start + 1) <=? a))
from the context (b ~ (end - start), (start + 1) <= end, end <= a)
bound by a pattern with constructor
Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
((start + 1) <= end, end <= numElements) =>
SNat numElements
-> SNat start -> SNat end -> Slice numElements (end - start),
in an equation for ‘heqHet'’
at Slice.hs:24:10-26
or from (b' ~ (end1 - start1), (start1 + 1) <= end1, end1 <= a)
bound by a pattern with constructor
Slice :: forall (numElements :: Nat) (start :: Nat) (end :: Nat).
((start + 1) <= end, end <= numElements) =>
SNat numElements
-> SNat start -> SNat end -> Slice numElements (end - start),
in an equation for ‘heqHet'’
at Slice.hs:24:30-48
NB: ‘GHC.TypeLits.<=?’ is a type function, and may not be injective
Relevant bindings include
heqHet' :: Slice a b -> Slice a b' -> Bool (bound at Slice.hs:24:1)
In the pattern: Slice _ start end
In an equation for ‘heqHet'’:
heqHet' (Slice _ start end) (Slice _ start' end')
| Just _ <- heqHet start start', Just _ <- heqHet end end' = True
| otherwise = False
Failed, modules loaded: none.
```

Trac field | Value |
---|---|

Version | 7.10.2 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |

Exactly what it says on the tin. It would be nice if the following would compile:

```
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :: Y ('X "hello" 4)
```

I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.

I'm a little out of my depth with rewrite rules, but is there anything preventing rules being associated with a typeclass? Then you could have zero method typeclasses like

```
class Functor f => LawfulFunctor f where
{-# RULES "fmap/coerce" fmap coerce = coerce #-}
```

and then any datatype that wants the rule just implements the typeclass, which is trivial. It would also address dfeuer's comment about lawfullness in constraints, though it would also generate a lot of noise in documentation (and might inherit the same issue with typeclasses that they can be hard to refactor).

I was tempted to say precedence rules are the same on the type level (implied by #6027 (closed)). Prefix `Foo`

should have higher precedence then any infix expression, and I *thought* that infix type operators took the same precedence as their value level versions (though what precedence ~ gets I'm not sure, but I guess it's low), though when I tried to construct a quick example to illustrate in GHCi I didn't get that behaviour:

```
type family a + b
type instance a + b = a
type family a * b
type instance a * b = b
:kind! Int + Bool * Char
Int + Bool * Char :: *
= Char
:kind! Int + (Bool * Char)
Int + (Bool * Char) :: *
= Int
```

:/

I wrote a proposal for the explicitly imported identifiers case here [1], which was discussed here [2]. #9702 is also relevant.

[1] https://www.haskell.org/haskellwiki/PermissiveImportsProposal [2] https://www.haskell.org/pipermail/glasgow-haskell-users/2014-October/025306.html