Commit b5565f1a authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #11711.

There were two bugs here, both simple: we need to filter out
covars before calling isMetaTyVar in the solver, and TcPat had
a tcSubType the wrong way round.

test case: dependent/should_compile/T11711
parent 46f9a476
......@@ -419,9 +419,11 @@ pprPat (TuplePat pats bx _) = tupleParens (boxityTupleSort bx) (pprWithCommas
pprPat (ConPatIn con details) = pprUserCon (unLoc con) details
pprPat (ConPatOut { pat_con = con, pat_tvs = tvs, pat_dicts = dicts,
pat_binds = binds, pat_args = details })
= getPprStyle $ \ sty -> -- Tiresome; in TcBinds.tcRhs we print out a
if debugStyle sty then -- typechecked Pat in an error message,
-- and we want to make sure it prints nicely
= sdocWithDynFlags $ \dflags ->
-- Tiresome; in TcBinds.tcRhs we print out a
-- typechecked Pat in an error message,
-- and we want to make sure it prints nicely
if gopt Opt_PrintTypecheckerElaboration dflags then
ppr con
<> braces (sep [ hsep (map pprPatBndr (tvs ++ dicts))
, ppr binds])
......
......@@ -816,7 +816,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
prov_theta' = substTheta tenv prov_theta
req_theta' = substTheta tenv req_theta
; wrap <- tcSubTypeO (pe_orig penv) GenSigCtxt ty' pat_ty
; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
; traceTc "tcPatSynPat" (ppr pat_syn $$
ppr pat_ty $$
ppr ty' $$
......
......@@ -125,10 +125,12 @@ simpl_top wanteds
= return wc
| otherwise
= do { free_tvs <- TcS.zonkTyCoVarsAndFV (tyCoVarsOfWC wc)
; let meta_tvs = varSetElems (filterVarSet isMetaTyVar free_tvs)
; let meta_tvs = varSetElems $
filterVarSet (isTyVar <&&> isMetaTyVar) free_tvs
-- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
-- filter isMetaTyVar: we might have runtime-skolems in GHCi,
-- and we definitely don't want to try to assign to those!
-- the isTyVar needs to weed out coercion variables
; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
; if or defaulted
......
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
module T11711 where
import Data.Kind (Type)
data (:~~:) (a :: k1) (b :: k2) where
HRefl :: a :~~: a
data TypeRep (a :: k) where
TrTyCon :: String -> TypeRep k -> TypeRep (a :: k)
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
class Typeable (a :: k) where
typeRep :: TypeRep a
data TypeRepX where
TypeRepX :: forall k (a :: k). TypeRep a -> TypeRepX
eqTypeRep :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind = undefined
instance Typeable Type where
typeRep = TrTyCon "Type" typeRep
funResultTy :: TypeRepX -> TypeRepX -> Maybe TypeRepX
funResultTy (TypeRepX f) (TypeRepX x)
| Just HRefl <- (typeRep :: TypeRep Type) `eqTypeRep` typeRepKind f
, TRFun arg res <- f
, Just HRefl <- arg `eqTypeRep` x
= Just (TypeRepX res)
| otherwise
= Nothing
trArrow :: TypeRep (->)
trArrow = undefined
pattern TRFun :: forall fun. ()
=> forall arg res. (fun ~ (arg -> res))
=> TypeRep arg
-> TypeRep res
-> TypeRep fun
pattern TRFun arg res <- TrApp (TrApp (eqTypeRep trArrow -> Just HRefl) arg) res
......@@ -17,3 +17,4 @@ test('dynamic-paper', expect_fail_for(['optasm', 'optllvm']), compile, [''])
test('T11311', normal, compile, [''])
test('T11405', normal, compile, [''])
test('T11241', normal, compile, [''])
test('T11711', normal, compile, [''])
mono.hs:7:4:
Couldn't match type ‘Int’ with ‘Bool
Expected type: [Bool]
Actual type: [Int]
In the pattern: Single x
In an equation for ‘f’: f (Single x) = x
mono.hs:7:4: error:
• Couldn't match type ‘Bool’ with ‘Int
Expected type: [Int]
Actual type: [Bool]
In the pattern: Single x
In an equation for ‘f’: f (Single x) = x
mono.hs:7:16:
Couldn't match expected type ‘Bool’ with actual type ‘Int’
In the expression: x
In an equation for ‘f’: f (Single x) = x
mono.hs:7:16: error:
Couldn't match expected type ‘Bool’ with actual type ‘Int’
In the expression: x
In an equation for ‘f’: f (Single x) = x
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