Commit 70ddb8bf authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Add regression test for #17773

parent 9c89a48d
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(..))
type family (x :: f a) <|> (y :: f a) :: f a
type family Mzero :: f a
monadPlusMplus :: forall f a (x :: f a) (y :: f a).
Proxy x -> Proxy y
-> Mzero x y :~: (x <|> y)
monadPlusMplus _ _ = _Refl
T17773.hs:16:22: error:
• Found hole: _Refl :: Mzero x y :~: (x <|> y)
Where: ‘x’, ‘f’, ‘k’, ‘a’, ‘y’ are rigid type variables bound by
the type signature for:
monadPlusMplus :: forall k (f :: k -> *) (a :: k) (x :: f a)
(y :: f a).
Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
at T17773.hs:(13,1)-(15,41)
Or perhaps ‘_Refl’ is mis-spelled, or not in scope
• In the expression: _Refl
In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl
• Relevant bindings include
monadPlusMplus :: Proxy x -> Proxy y -> Mzero x y :~: (x <|> y)
(bound at T17773.hs:16:1)
......@@ -552,3 +552,4 @@ test('T17563', normal, compile_fail, [''])
test('T16946', normal, compile_fail, [''])
test('T17566b', normal, compile_fail, [''])
test('T17566c', normal, compile_fail, [''])
test('T17773', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment